Let J and f be given.
Assume Hf: f ∈ power_real J.
Apply (xm (J = Empty)) to the current goal.
Assume HJ0: J = Empty.
We prove the intermediate claim Hdef: power_real_uniform_metric_value J f f = If_i (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J f f) r)).
Use reflexivity.
rewrite the current goal using Hdef (from left to right).
rewrite the current goal using (If_i_1 (J = Empty) 0 (Eps_i (λr : set ⇒ R_lub (power_real_clipped_diffs J f f) r)) HJ0) (from left to right).
Use reflexivity.
Assume HJne: ¬ (J = Empty).
We prove the intermediate claim HJne2: J ≠ Empty.
An exact proof term for the current goal is HJne.
Set A to be the term power_real_clipped_diffs J f f.
We prove the intermediate claim HAeq: A = {0}.
An exact proof term for the current goal is (power_real_clipped_diffs_diag_eq_Sing0 J f HJne2 Hf).
We prove the intermediate claim Hlub1: R_lub A (power_real_uniform_metric_value J f f).
An exact proof term for the current goal is (power_real_uniform_metric_value_is_lub J f f HJne2 Hf Hf).
We prove the intermediate claim Hlub0: R_lub A 0.
rewrite the current goal using HAeq (from left to right).
An exact proof term for the current goal is R_lub_Sing0.
An exact proof term for the current goal is (R_lub_unique A (power_real_uniform_metric_value J f f) 0 Hlub1 Hlub0).
∎