Let X, d, x, A and eps be given.
Assume Hm: metric_on X d.
Assume HxX: x ∈ X.
Assume HAsub: A ⊆ X.
Assume HAne: A ≠ Empty.
Assume HepsR: eps ∈ R.
Assume HepsPos: Rlt 0 eps.
Set S to be the term metric_neg_dists X d x A.
Set l to be the term metric_sup_neg_dists X d x A.
We prove the intermediate claim Hlub: R_lub S l.
An exact proof term for the current goal is (metric_sup_neg_dists_is_lub X d x A Hm HxX HAsub HAne).
We prove the intermediate claim HlR: l ∈ R.
An exact proof term for the current goal is (R_lub_in_R S l Hlub).
We prove the intermediate claim HdistR: metric_dist_to_set X d x A ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x A Hm HxX HAsub HAne).
We prove the intermediate claim HdistDef: metric_dist_to_set X d x A = minus_SNo l.
Use reflexivity.
We prove the intermediate claim Hex: ∃t : set, t ∈ S ∧ t ∈ R ∧ Rlt (add_SNo l (minus_SNo eps)) t.
An exact proof term for the current goal is (R_lub_approx_from_below S l eps Hlub HepsR HepsPos).
Apply Hex to the current goal.
Let t be given.
Assume Htpack.
We prove the intermediate claim HtCore: t ∈ S ∧ t ∈ R.
An exact proof term for the current goal is (andEL (t ∈ S ∧ t ∈ R) (Rlt (add_SNo l (minus_SNo eps)) t) Htpack).
We prove the intermediate claim HtIn: t ∈ S.
An exact proof term for the current goal is (andEL (t ∈ S) (t ∈ R) HtCore).
Apply (ReplE_impred A (λa0 : set ⇒ minus_SNo (apply_fun d (x,a0))) t HtIn (∃a : set, a ∈ A ∧ a ∈ X ∧ Rlt (apply_fun d (x,a)) (add_SNo (metric_dist_to_set X d x A) eps))) to the current goal.
Let a be given.
Assume HaA: a ∈ A.
Assume Hteq: t = minus_SNo (apply_fun d (x,a)).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsub a HaA).
We prove the intermediate claim Hfun: function_on d (setprod X X) R.
An exact proof term for the current goal is (metric_on_function_on X d Hm).
We prove the intermediate claim HxaIn: (x,a) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x a HxX HaX).
We prove the intermediate claim HdxaR: apply_fun d (x,a) ∈ R.
An exact proof term for the current goal is (Hfun (x,a) HxaIn).
We prove the intermediate claim HtR: t ∈ R.
An exact proof term for the current goal is (andER (t ∈ S) (t ∈ R) HtCore).
We prove the intermediate claim Hlt: Rlt (add_SNo l (minus_SNo eps)) t.
An exact proof term for the current goal is (andER (t ∈ S ∧ t ∈ R) (Rlt (add_SNo l (minus_SNo eps)) t) Htpack).
We prove the intermediate claim HltS: add_SNo l (minus_SNo eps) < t.
An exact proof term for the current goal is (RltE_lt (add_SNo l (minus_SNo eps)) t Hlt).
We prove the intermediate claim HlS: SNo l.
An exact proof term for the current goal is (real_SNo l HlR).
We prove the intermediate claim HepsS: SNo eps.
An exact proof term for the current goal is (real_SNo eps HepsR).
We prove the intermediate claim HmepsR: minus_SNo eps ∈ R.
An exact proof term for the current goal is (real_minus_SNo eps HepsR).
We prove the intermediate claim HmepsS: SNo (minus_SNo eps).
An exact proof term for the current goal is (real_SNo (minus_SNo eps) HmepsR).
We prove the intermediate claim HsumS: SNo (add_SNo l (minus_SNo eps)).
An exact proof term for the current goal is (real_SNo (add_SNo l (minus_SNo eps)) (real_add_SNo l HlR (minus_SNo eps) HmepsR)).
We prove the intermediate claim HdxaS: SNo (apply_fun d (x,a)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x,a)) HdxaR).
We prove the intermediate claim HtS: SNo t.
An exact proof term for the current goal is (real_SNo t HtR).
We prove the intermediate claim HltS2: add_SNo l (minus_SNo eps) < minus_SNo (apply_fun d (x,a)).
rewrite the current goal using Hteq (from right to left).
An exact proof term for the current goal is HltS.
We prove the intermediate claim Hneg: apply_fun d (x,a) < minus_SNo (add_SNo l (minus_SNo eps)).
We prove the intermediate claim Hneg1: minus_SNo (minus_SNo (apply_fun d (x,a))) < minus_SNo (add_SNo l (minus_SNo eps)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (add_SNo l (minus_SNo eps)) (minus_SNo (apply_fun d (x,a))) HsumS (SNo_minus_SNo (apply_fun d (x,a)) HdxaS) HltS2).
We prove the intermediate claim Hinv: minus_SNo (minus_SNo (apply_fun d (x,a))) = apply_fun d (x,a).
An exact proof term for the current goal is (minus_SNo_minus_SNo_real (apply_fun d (x,a)) HdxaR).
rewrite the current goal using Hinv (from right to left).
An exact proof term for the current goal is Hneg1.
We prove the intermediate claim HrhsEq: minus_SNo (add_SNo l (minus_SNo eps)) = add_SNo (minus_SNo l) eps.
rewrite the current goal using (minus_add_SNo_distr l (minus_SNo eps) HlS HmepsS) (from left to right).
rewrite the current goal using (minus_SNo_minus_SNo_real eps HepsR) (from left to right).
Use reflexivity.
We prove the intermediate claim HltR2: Rlt (apply_fun d (x,a)) (add_SNo (minus_SNo l) eps).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is (RltI (apply_fun d (x,a)) (minus_SNo (add_SNo l (minus_SNo eps))) HdxaR (real_minus_SNo (add_SNo l (minus_SNo eps)) (real_add_SNo l HlR (minus_SNo eps) HmepsR)) Hneg).
We use a to witness the existential quantifier.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is HaA.
An exact proof term for the current goal is HaX.
rewrite the current goal using HdistDef (from left to right).
An exact proof term for the current goal is HltR2.
∎