Let X and d be given.
Assume Hd: metric_on X d.
We will prove normal_space X (metric_topology X d).
We will prove one_point_sets_closed X (metric_topology X d) ∧ ∀A B : set, closed_in X (metric_topology X d) A → closed_in X (metric_topology X d) B → A ∩ B = Empty → ∃U V : set, U ∈ (metric_topology X d) ∧ V ∈ (metric_topology X d) ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_topology_one_point_sets_closed X d Hd).
Let A and B be given.
Assume HAcl: closed_in X (metric_topology X d) A.
Assume HBcl: closed_in X (metric_topology X d) B.
Assume Hdisj: A ∩ B = Empty.
We will prove ∃U V : set, U ∈ (metric_topology X d) ∧ V ∈ (metric_topology X d) ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
We prove the intermediate claim HTx: topology_on X (metric_topology X d).
An exact proof term for the current goal is (metric_topology_is_topology X d Hd).
Apply (xm (A = Empty)) to the current goal.
Assume HAe: A = Empty.
We use Empty to witness the existential quantifier.
We use X to witness the existential quantifier.
We will prove Empty ∈ metric_topology X d ∧ X ∈ metric_topology X d ∧ A ⊆ Empty ∧ B ⊆ X ∧ Empty ∩ X = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_empty X (metric_topology X d) HTx).
An exact proof term for the current goal is (topology_has_X X (metric_topology X d) HTx).
rewrite the current goal using HAe (from left to right).
An exact proof term for the current goal is (Subq_Empty Empty).
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) B HBcl).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ Empty ∩ X.
We will prove x ∈ Empty.
An exact proof term for the current goal is (binintersectE1 Empty X x Hx).
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ Empty ∩ X.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ Empty ∩ X)).
Assume HAn: ¬ (A = Empty).
Apply (xm (B = Empty)) to the current goal.
Assume HBe: B = Empty.
We use X to witness the existential quantifier.
We use Empty to witness the existential quantifier.
We will prove X ∈ metric_topology X d ∧ Empty ∈ metric_topology X d ∧ A ⊆ X ∧ B ⊆ Empty ∧ X ∩ Empty = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
An exact proof term for the current goal is (topology_has_X X (metric_topology X d) HTx).
An exact proof term for the current goal is (topology_has_empty X (metric_topology X d) HTx).
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) A HAcl).
rewrite the current goal using HBe (from left to right).
An exact proof term for the current goal is (Subq_Empty Empty).
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ X ∩ Empty.
We will prove x ∈ Empty.
An exact proof term for the current goal is (binintersectE2 X Empty x Hx).
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ X ∩ Empty.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ X ∩ Empty)).
Assume HBn: ¬ (B = Empty).
Set U to be the term {x ∈ X|Rlt (metric_dist_to_set X d x A) (metric_dist_to_set X d x B)}.
Set V to be the term {x ∈ X|Rlt (metric_dist_to_set X d x B) (metric_dist_to_set X d x A)}.
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
We will prove U ∈ metric_topology X d ∧ V ∈ metric_topology X d ∧ A ⊆ U ∧ B ⊆ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
Apply andI to the current goal.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) B HBcl).
Set B0 to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r0|r0 ∈ R, Rlt 0 r0}).
We prove the intermediate claim HTdef: metric_topology X d = generated_topology X B0.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We will prove U ∈ generated_topology X B0.
We prove the intermediate claim HUsubX0: U ⊆ X.
Let x0 be given.
Assume Hx0U: x0 ∈ U.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 A) (metric_dist_to_set X d z0 B)) x0 Hx0U).
We prove the intermediate claim HUPow: U ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X U HUsubX0).
We prove the intermediate claim HUprop: ∀x0 ∈ U, ∃b ∈ B0, x0 ∈ b ∧ b ⊆ U.
Let x0 be given.
Assume Hx0U: x0 ∈ U.
We will prove ∃b ∈ B0, x0 ∈ b ∧ b ⊆ U.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 A) (metric_dist_to_set X d z0 B)) x0 Hx0U).
We prove the intermediate claim Hx0lt: Rlt (metric_dist_to_set X d x0 A) (metric_dist_to_set X d x0 B).
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 A) (metric_dist_to_set X d z0 B)) x0 Hx0U).
Set distA0 to be the term metric_dist_to_set X d x0 A.
Set distB0 to be the term metric_dist_to_set X d x0 B.
We prove the intermediate claim HdistA0R: distA0 ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x0 A Hd Hx0X HAsubX HAn).
We prove the intermediate claim HdistB0R: distB0 ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x0 B Hd Hx0X HBsubX HBn).
Set gap to be the term add_SNo distB0 (minus_SNo distA0).
We prove the intermediate claim HgapPos: Rlt 0 gap.
An exact proof term for the current goal is (Rlt_0_diff_of_lt distA0 distB0 Hx0lt).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (RltE_right 0 gap HgapPos).
We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < gap.
An exact proof term for the current goal is (exists_eps_lt_pos gap HgapR HgapPos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < gap) HN0pair).
We prove the intermediate claim HepsN0lt: eps_ N0 < gap.
An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < gap) HN0pair).
We prove the intermediate claim HepsN0R: eps_ N0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N0) (SNo_eps_SNoS_omega N0 HN0omega)).
We prove the intermediate claim HepsN0Rlt: Rlt (eps_ N0) gap.
An exact proof term for the current goal is (RltI (eps_ N0) gap HepsN0R HgapR HepsN0lt).
We prove the intermediate claim HN0nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
We prove the intermediate claim Hsucc0: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).
Set r to be the term eps_ (ordsucc N0).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r (SNo_eps_SNoS_omega (ordsucc N0) Hsucc0)).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N0) Hsucc0).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (RltI 0 r real_0 HrR HrposS).
We prove the intermediate claim HrrEq: add_SNo r r = eps_ N0.
An exact proof term for the current goal is (eps_ordsucc_half_add N0 HN0nat).
We prove the intermediate claim HrrR: add_SNo r r ∈ R.
An exact proof term for the current goal is (real_add_SNo r HrR r HrR).
We prove the intermediate claim HrrLtGap: Rlt (add_SNo r r) gap.
rewrite the current goal using HrrEq (from left to right).
An exact proof term for the current goal is HepsN0Rlt.
We prove the intermediate claim Hmargin: Rlt (add_SNo distA0 r) (add_SNo distB0 (minus_SNo r)).
We prove the intermediate claim HdistA0S: SNo distA0.
An exact proof term for the current goal is (real_SNo distA0 HdistA0R).
We prove the intermediate claim HdistB0S: SNo distB0.
An exact proof term for the current goal is (real_SNo distB0 HdistB0R).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HgapS: SNo gap.
An exact proof term for the current goal is (real_SNo gap HgapR).
We prove the intermediate claim HrrS: SNo (add_SNo r r).
An exact proof term for the current goal is (real_SNo (add_SNo r r) HrrR).
We prove the intermediate claim HrrLtGapS: add_SNo r r < gap.
An exact proof term for the current goal is (RltE_lt (add_SNo r r) gap HrrLtGap).
We prove the intermediate claim HlhsR: add_SNo distA0 (add_SNo r r) ∈ R.
An exact proof term for the current goal is (real_add_SNo distA0 HdistA0R (add_SNo r r) HrrR).
We prove the intermediate claim Hr2R: add_SNo distB0 (minus_SNo distA0) ∈ R.
An exact proof term for the current goal is (real_add_SNo distB0 HdistB0R (minus_SNo distA0) (real_minus_SNo distA0 HdistA0R)).
We prove the intermediate claim HtmpLt: add_SNo distA0 (add_SNo r r) < add_SNo distA0 gap.
An exact proof term for the current goal is (add_SNo_Lt2 distA0 (add_SNo r r) gap HdistA0S HrrS HgapS HrrLtGapS).
We prove the intermediate claim HtmpRlt: Rlt (add_SNo distA0 (add_SNo r r)) (add_SNo distA0 gap).
An exact proof term for the current goal is (RltI (add_SNo distA0 (add_SNo r r)) (add_SNo distA0 gap) HlhsR (real_add_SNo distA0 HdistA0R gap HgapR) HtmpLt).
We prove the intermediate claim HgapEq: add_SNo distA0 gap = distB0.
rewrite the current goal using (add_SNo_assoc distA0 distB0 (minus_SNo distA0) HdistA0S HdistB0S (real_SNo (minus_SNo distA0) (real_minus_SNo distA0 HdistA0R))) (from left to right).
rewrite the current goal using (add_SNo_com distA0 distB0 HdistA0S HdistB0S) (from left to right).
rewrite the current goal using (add_SNo_assoc distB0 distA0 (minus_SNo distA0) HdistB0S HdistA0S (real_SNo (minus_SNo distA0) (real_minus_SNo distA0 HdistA0R))) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv distA0 HdistA0S) (from left to right).
rewrite the current goal using (add_SNo_0R distB0 HdistB0S) (from left to right).
Use reflexivity.
We prove the intermediate claim HtmpRlt2: Rlt (add_SNo distA0 (add_SNo r r)) distB0.
rewrite the current goal using HgapEq (from right to left).
An exact proof term for the current goal is HtmpRlt.
We prove the intermediate claim HminusR: minus_SNo r ∈ R.
An exact proof term for the current goal is (real_minus_SNo r HrR).
We prove the intermediate claim HminusS: SNo (minus_SNo r).
An exact proof term for the current goal is (real_SNo (minus_SNo r) HminusR).
We prove the intermediate claim HaddLe: Rlt (add_SNo (add_SNo distA0 (add_SNo r r)) (minus_SNo r)) (add_SNo distB0 (minus_SNo r)).
An exact proof term for the current goal is (RltI (add_SNo (add_SNo distA0 (add_SNo r r)) (minus_SNo r)) (add_SNo distB0 (minus_SNo r)) (real_add_SNo (add_SNo distA0 (add_SNo r r)) HlhsR (minus_SNo r) HminusR) (real_add_SNo distB0 HdistB0R (minus_SNo r) HminusR) (add_SNo_Lt1 (add_SNo distA0 (add_SNo r r)) (minus_SNo r) distB0 (real_SNo (add_SNo distA0 (add_SNo r r)) HlhsR) HminusS HdistB0S (RltE_lt (add_SNo distA0 (add_SNo r r)) distB0 HtmpRlt2))).
We prove the intermediate claim HlhsEq: add_SNo (add_SNo distA0 (add_SNo r r)) (minus_SNo r) = add_SNo distA0 r.
rewrite the current goal using (add_SNo_assoc distA0 r r HdistA0S HrS HrS) (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo distA0 r) r (minus_SNo r) (real_SNo (add_SNo distA0 r) (real_add_SNo distA0 HdistA0R r HrR)) HrS HminusS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv r HrS) (from left to right).
rewrite the current goal using (add_SNo_0R (add_SNo distA0 r) (real_SNo (add_SNo distA0 r) (real_add_SNo distA0 HdistA0R r HrR))) (from left to right).
Use reflexivity.
We prove the intermediate claim HaddLe2: Rlt (add_SNo distA0 r) (add_SNo distB0 (minus_SNo r)).
rewrite the current goal using HlhsEq (from right to left).
An exact proof term for the current goal is HaddLe.
An exact proof term for the current goal is HaddLe2.
We use (open_ball X d x0 r) to witness the existential quantifier.
We will prove open_ball X d x0 r ∈ B0 ∧ (x0 ∈ open_ball X d x0 r ∧ open_ball X d x0 r ⊆ U).
Apply andI to the current goal.
We prove the intermediate claim HballIn: open_ball X d x0 r ∈ {open_ball X d x0 r0|r0 ∈ R, Rlt 0 r0}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) r HrR Hrpos).
An exact proof term for the current goal is (famunionI X (λx1 : set ⇒ {open_ball X d x1 r0|r0 ∈ R, Rlt 0 r0}) x0 (open_ball X d x0 r) Hx0X HballIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball X d x0 r Hd Hx0X Hrpos).
Let y0 be given.
Assume Hy0Ball: y0 ∈ open_ball X d x0 r.
We will prove y0 ∈ U.
We prove the intermediate claim Hy0X: y0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (apply_fun d (x0,z0)) r) y0 Hy0Ball).
We prove the intermediate claim Hdxy0: Rlt (apply_fun d (x0,y0)) r.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ Rlt (apply_fun d (x0,z0)) r) y0 Hy0Ball).
We prove the intermediate claim Hdxy0R: apply_fun d (x0,y0) ∈ R.
An exact proof term for the current goal is (metric_on_function_on X d Hd (x0,y0) (tuple_2_setprod_by_pair_Sigma X X x0 y0 Hx0X Hy0X)).
We prove the intermediate claim HleA: Rle (metric_dist_to_set X d y0 A) (add_SNo distA0 (apply_fun d (x0,y0))).
An exact proof term for the current goal is (metric_dist_to_set_Lipschitz X d x0 y0 A Hd Hx0X Hy0X HAsubX HAn).
We prove the intermediate claim HltA1: Rlt (add_SNo distA0 (apply_fun d (x0,y0))) (add_SNo distA0 r).
We prove the intermediate claim HdistA0S: SNo distA0.
An exact proof term for the current goal is (real_SNo distA0 HdistA0R).
We prove the intermediate claim Hdxy0S: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
An exact proof term for the current goal is (RltI (add_SNo distA0 (apply_fun d (x0,y0))) (add_SNo distA0 r) (real_add_SNo distA0 HdistA0R (apply_fun d (x0,y0)) Hdxy0R) (real_add_SNo distA0 HdistA0R r HrR) (add_SNo_Lt2 distA0 (apply_fun d (x0,y0)) r HdistA0S Hdxy0S HrS (RltE_lt (apply_fun d (x0,y0)) r Hdxy0))).
We prove the intermediate claim HltA: Rlt (metric_dist_to_set X d y0 A) (add_SNo distA0 r).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (metric_dist_to_set X d y0 A) (add_SNo distA0 (apply_fun d (x0,y0))) (add_SNo distA0 r) HleA HltA1).
We prove the intermediate claim HleBswap: Rle distB0 (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (y0,x0))).
An exact proof term for the current goal is (metric_dist_to_set_Lipschitz X d y0 x0 B Hd Hy0X Hx0X HBsubX HBn).
We prove the intermediate claim Hsymd: apply_fun d (y0,x0) = apply_fun d (x0,y0).
An exact proof term for the current goal is (metric_on_symmetric X d y0 x0 Hd Hy0X Hx0X).
We prove the intermediate claim HleB: Rle distB0 (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0))).
rewrite the current goal using Hsymd (from right to left).
An exact proof term for the current goal is HleBswap.
We prove the intermediate claim HlowerB: Rle (add_SNo distB0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 B).
We prove the intermediate claim HmdxyR: minus_SNo (apply_fun d (x0,y0)) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HmdxyS: SNo (minus_SNo (apply_fun d (x0,y0))).
An exact proof term for the current goal is (real_SNo (minus_SNo (apply_fun d (x0,y0))) HmdxyR).
We prove the intermediate claim HsumR: add_SNo (minus_SNo (apply_fun d (x0,y0))) distB0 ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo (apply_fun d (x0,y0))) HmdxyR distB0 HdistB0R).
We prove the intermediate claim HsumR2: add_SNo (minus_SNo (apply_fun d (x0,y0))) (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0))) ∈ R.
An exact proof term for the current goal is (real_add_SNo (minus_SNo (apply_fun d (x0,y0))) HmdxyR (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0))) (real_add_SNo (metric_dist_to_set X d y0 B) (metric_dist_to_set_in_R X d y0 B Hd Hy0X HBsubX HBn) (apply_fun d (x0,y0)) Hdxy0R)).
We prove the intermediate claim Hshift: Rle (add_SNo (minus_SNo (apply_fun d (x0,y0))) distB0) (add_SNo (minus_SNo (apply_fun d (x0,y0))) (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (minus_SNo (apply_fun d (x0,y0))) distB0 (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0))) HmdxyR HdistB0R (real_add_SNo (metric_dist_to_set X d y0 B) (metric_dist_to_set_in_R X d y0 B Hd Hy0X HBsubX HBn) (apply_fun d (x0,y0)) Hdxy0R) HleB).
We prove the intermediate claim HrhsEq: add_SNo (minus_SNo (apply_fun d (x0,y0))) (add_SNo (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0))) = metric_dist_to_set X d y0 B.
We prove the intermediate claim HdxyS: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HB0R: metric_dist_to_set X d y0 B ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d y0 B Hd Hy0X HBsubX HBn).
We prove the intermediate claim HB0S: SNo (metric_dist_to_set X d y0 B).
An exact proof term for the current goal is (real_SNo (metric_dist_to_set X d y0 B) HB0R).
We prove the intermediate claim HmdxyS2: SNo (minus_SNo (apply_fun d (x0,y0))).
An exact proof term for the current goal is (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)).
rewrite the current goal using (add_SNo_assoc (minus_SNo (apply_fun d (x0,y0))) (metric_dist_to_set X d y0 B) (apply_fun d (x0,y0)) HmdxyS2 HB0S HdxyS) (from left to right).
rewrite the current goal using (add_SNo_com (minus_SNo (apply_fun d (x0,y0))) (metric_dist_to_set X d y0 B) HmdxyS2 HB0S) (from left to right).
rewrite the current goal using (add_SNo_assoc (metric_dist_to_set X d y0 B) (minus_SNo (apply_fun d (x0,y0))) (apply_fun d (x0,y0)) HB0S HmdxyS2 HdxyS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv (apply_fun d (x0,y0)) HdxyS) (from left to right).
rewrite the current goal using (add_SNo_0R (metric_dist_to_set X d y0 B) HB0S) (from left to right).
Use reflexivity.
We prove the intermediate claim HlhsEq: add_SNo (minus_SNo (apply_fun d (x0,y0))) distB0 = add_SNo distB0 (minus_SNo (apply_fun d (x0,y0))).
We prove the intermediate claim HdistB0S: SNo distB0.
An exact proof term for the current goal is (real_SNo distB0 HdistB0R).
We prove the intermediate claim HmdxyS2: SNo (minus_SNo (apply_fun d (x0,y0))).
An exact proof term for the current goal is (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)).
An exact proof term for the current goal is (add_SNo_com (minus_SNo (apply_fun d (x0,y0))) distB0 HmdxyS2 HdistB0S).
We prove the intermediate claim Hshift2: Rle (add_SNo distB0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 B).
rewrite the current goal using HlhsEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is Hshift.
An exact proof term for the current goal is Hshift2.
We prove the intermediate claim HltB0: Rlt (add_SNo distB0 (minus_SNo r)) (add_SNo distB0 (minus_SNo (apply_fun d (x0,y0)))).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HdxyS: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HmdxyS: SNo (minus_SNo (apply_fun d (x0,y0))).
An exact proof term for the current goal is (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)).
We prove the intermediate claim HmrS: SNo (minus_SNo r).
An exact proof term for the current goal is (real_SNo (minus_SNo r) (real_minus_SNo r HrR)).
We prove the intermediate claim HdxyLtS: apply_fun d (x0,y0) < r.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x0,y0)) r Hdxy0).
We prove the intermediate claim HnegLt: minus_SNo r < minus_SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (apply_fun d (x0,y0)) r HdxyS HrS HdxyLtS).
An exact proof term for the current goal is (RltI (add_SNo distB0 (minus_SNo r)) (add_SNo distB0 (minus_SNo (apply_fun d (x0,y0)))) (real_add_SNo distB0 HdistB0R (minus_SNo r) (real_minus_SNo r HrR)) (real_add_SNo distB0 HdistB0R (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) (add_SNo_Lt2 distB0 (minus_SNo r) (minus_SNo (apply_fun d (x0,y0))) (real_SNo distB0 HdistB0R) (real_SNo (minus_SNo r) (real_minus_SNo r HrR)) (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) HnegLt)).
We prove the intermediate claim HltB: Rlt (add_SNo distB0 (minus_SNo r)) (metric_dist_to_set X d y0 B).
An exact proof term for the current goal is (Rlt_Rle_tra (add_SNo distB0 (minus_SNo r)) (add_SNo distB0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 B) HltB0 HlowerB).
We prove the intermediate claim HltMid: Rlt (add_SNo distA0 r) (metric_dist_to_set X d y0 B).
An exact proof term for the current goal is (Rlt_tra (add_SNo distA0 r) (add_SNo distB0 (minus_SNo r)) (metric_dist_to_set X d y0 B) Hmargin HltB).
Apply (SepI X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 A) (metric_dist_to_set X d z0 B)) y0 Hy0X) to the current goal.
An exact proof term for the current goal is (Rlt_tra (metric_dist_to_set X d y0 A) (add_SNo distA0 r) (metric_dist_to_set X d y0 B) HltA HltMid).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀x0 ∈ U0, ∃b ∈ B0, x0 ∈ b ∧ b ⊆ U0) U HUPow HUprop).
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) B HBcl).
Set B0 to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r0|r0 ∈ R, Rlt 0 r0}).
We prove the intermediate claim HTdef: metric_topology X d = generated_topology X B0.
Use reflexivity.
rewrite the current goal using HTdef (from left to right).
We will prove V ∈ generated_topology X B0.
We prove the intermediate claim HVsubX0: V ⊆ X.
Let x0 be given.
Assume Hx0V: x0 ∈ V.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 B) (metric_dist_to_set X d z0 A)) x0 Hx0V).
We prove the intermediate claim HVPow: V ∈ 𝒫 X.
An exact proof term for the current goal is (PowerI X V HVsubX0).
We prove the intermediate claim HVprop: ∀x0 ∈ V, ∃b ∈ B0, x0 ∈ b ∧ b ⊆ V.
Let x0 be given.
Assume Hx0V: x0 ∈ V.
We will prove ∃b ∈ B0, x0 ∈ b ∧ b ⊆ V.
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 B) (metric_dist_to_set X d z0 A)) x0 Hx0V).
We prove the intermediate claim Hx0lt: Rlt (metric_dist_to_set X d x0 B) (metric_dist_to_set X d x0 A).
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 B) (metric_dist_to_set X d z0 A)) x0 Hx0V).
Set distA0 to be the term metric_dist_to_set X d x0 A.
Set distB0 to be the term metric_dist_to_set X d x0 B.
We prove the intermediate claim HdistA0R: distA0 ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x0 A Hd Hx0X HAsubX HAn).
We prove the intermediate claim HdistB0R: distB0 ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d x0 B Hd Hx0X HBsubX HBn).
Set gap to be the term add_SNo distA0 (minus_SNo distB0).
We prove the intermediate claim HgapPos: Rlt 0 gap.
An exact proof term for the current goal is (Rlt_0_diff_of_lt distB0 distA0 Hx0lt).
We prove the intermediate claim HgapR: gap ∈ R.
An exact proof term for the current goal is (RltE_right 0 gap HgapPos).
We prove the intermediate claim HexN0: ∃N0 ∈ ω, eps_ N0 < gap.
An exact proof term for the current goal is (exists_eps_lt_pos gap HgapR HgapPos).
Apply HexN0 to the current goal.
Let N0 be given.
Assume HN0pair.
We prove the intermediate claim HN0omega: N0 ∈ ω.
An exact proof term for the current goal is (andEL (N0 ∈ ω) (eps_ N0 < gap) HN0pair).
We prove the intermediate claim HepsN0lt: eps_ N0 < gap.
An exact proof term for the current goal is (andER (N0 ∈ ω) (eps_ N0 < gap) HN0pair).
We prove the intermediate claim HepsN0R: eps_ N0 ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N0) (SNo_eps_SNoS_omega N0 HN0omega)).
We prove the intermediate claim HepsN0Rlt: Rlt (eps_ N0) gap.
An exact proof term for the current goal is (RltI (eps_ N0) gap HepsN0R HgapR HepsN0lt).
We prove the intermediate claim HN0nat: nat_p N0.
An exact proof term for the current goal is (omega_nat_p N0 HN0omega).
We prove the intermediate claim Hsucc0: ordsucc N0 ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N0 HN0omega).
Set r to be the term eps_ (ordsucc N0).
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (SNoS_omega_real r (SNo_eps_SNoS_omega (ordsucc N0) Hsucc0)).
We prove the intermediate claim HrposS: 0 < r.
An exact proof term for the current goal is (SNo_eps_pos (ordsucc N0) Hsucc0).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (RltI 0 r real_0 HrR HrposS).
We prove the intermediate claim HrrEq: add_SNo r r = eps_ N0.
An exact proof term for the current goal is (eps_ordsucc_half_add N0 HN0nat).
We prove the intermediate claim HrrR: add_SNo r r ∈ R.
An exact proof term for the current goal is (real_add_SNo r HrR r HrR).
We prove the intermediate claim HrrLtGap: Rlt (add_SNo r r) gap.
rewrite the current goal using HrrEq (from left to right).
An exact proof term for the current goal is HepsN0Rlt.
We prove the intermediate claim Hmargin: Rlt (add_SNo distB0 r) (add_SNo distA0 (minus_SNo r)).
We prove the intermediate claim HdistA0S: SNo distA0.
An exact proof term for the current goal is (real_SNo distA0 HdistA0R).
We prove the intermediate claim HdistB0S: SNo distB0.
An exact proof term for the current goal is (real_SNo distB0 HdistB0R).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HgapS: SNo gap.
An exact proof term for the current goal is (real_SNo gap HgapR).
We prove the intermediate claim HrrS: SNo (add_SNo r r).
An exact proof term for the current goal is (real_SNo (add_SNo r r) HrrR).
We prove the intermediate claim HrrLtGapS: add_SNo r r < gap.
An exact proof term for the current goal is (RltE_lt (add_SNo r r) gap HrrLtGap).
We prove the intermediate claim HlhsR: add_SNo distB0 (add_SNo r r) ∈ R.
An exact proof term for the current goal is (real_add_SNo distB0 HdistB0R (add_SNo r r) HrrR).
We prove the intermediate claim HtmpLt: add_SNo distB0 (add_SNo r r) < add_SNo distB0 gap.
An exact proof term for the current goal is (add_SNo_Lt2 distB0 (add_SNo r r) gap HdistB0S HrrS HgapS HrrLtGapS).
We prove the intermediate claim HtmpRlt: Rlt (add_SNo distB0 (add_SNo r r)) (add_SNo distB0 gap).
An exact proof term for the current goal is (RltI (add_SNo distB0 (add_SNo r r)) (add_SNo distB0 gap) HlhsR (real_add_SNo distB0 HdistB0R gap HgapR) HtmpLt).
We prove the intermediate claim HgapEq: add_SNo distB0 gap = distA0.
We prove the intermediate claim HdistA0S2: SNo distA0.
An exact proof term for the current goal is (real_SNo distA0 HdistA0R).
We prove the intermediate claim HdistB0S2: SNo distB0.
An exact proof term for the current goal is (real_SNo distB0 HdistB0R).
We prove the intermediate claim HmB: SNo (minus_SNo distB0).
An exact proof term for the current goal is (real_SNo (minus_SNo distB0) (real_minus_SNo distB0 HdistB0R)).
rewrite the current goal using (add_SNo_assoc distB0 distA0 (minus_SNo distB0) HdistB0S2 HdistA0S2 HmB) (from left to right).
rewrite the current goal using (add_SNo_com distB0 distA0 HdistB0S2 HdistA0S2) (from left to right).
rewrite the current goal using (add_SNo_assoc distA0 distB0 (minus_SNo distB0) HdistA0S2 HdistB0S2 HmB) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv distB0 HdistB0S2) (from left to right).
rewrite the current goal using (add_SNo_0R distA0 HdistA0S2) (from left to right).
Use reflexivity.
We prove the intermediate claim HtmpRlt2: Rlt (add_SNo distB0 (add_SNo r r)) distA0.
rewrite the current goal using HgapEq (from right to left).
An exact proof term for the current goal is HtmpRlt.
We prove the intermediate claim HminusR: minus_SNo r ∈ R.
An exact proof term for the current goal is (real_minus_SNo r HrR).
We prove the intermediate claim HminusS: SNo (minus_SNo r).
An exact proof term for the current goal is (real_SNo (minus_SNo r) HminusR).
We prove the intermediate claim HaddLe: Rlt (add_SNo (add_SNo distB0 (add_SNo r r)) (minus_SNo r)) (add_SNo distA0 (minus_SNo r)).
An exact proof term for the current goal is (RltI (add_SNo (add_SNo distB0 (add_SNo r r)) (minus_SNo r)) (add_SNo distA0 (minus_SNo r)) (real_add_SNo (add_SNo distB0 (add_SNo r r)) HlhsR (minus_SNo r) HminusR) (real_add_SNo distA0 HdistA0R (minus_SNo r) HminusR) (add_SNo_Lt1 (add_SNo distB0 (add_SNo r r)) (minus_SNo r) distA0 (real_SNo (add_SNo distB0 (add_SNo r r)) HlhsR) HminusS (real_SNo distA0 HdistA0R) (RltE_lt (add_SNo distB0 (add_SNo r r)) distA0 HtmpRlt2))).
We prove the intermediate claim HlhsEq: add_SNo (add_SNo distB0 (add_SNo r r)) (minus_SNo r) = add_SNo distB0 r.
rewrite the current goal using (add_SNo_assoc distB0 r r (real_SNo distB0 HdistB0R) (real_SNo r HrR) (real_SNo r HrR)) (from left to right).
rewrite the current goal using (add_SNo_assoc (add_SNo distB0 r) r (minus_SNo r) (real_SNo (add_SNo distB0 r) (real_add_SNo distB0 HdistB0R r HrR)) (real_SNo r HrR) (real_SNo (minus_SNo r) (real_minus_SNo r HrR))) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_rinv r (real_SNo r HrR)) (from left to right).
rewrite the current goal using (add_SNo_0R (add_SNo distB0 r) (real_SNo (add_SNo distB0 r) (real_add_SNo distB0 HdistB0R r HrR))) (from left to right).
Use reflexivity.
We prove the intermediate claim HaddLe2: Rlt (add_SNo distB0 r) (add_SNo distA0 (minus_SNo r)).
rewrite the current goal using HlhsEq (from right to left).
An exact proof term for the current goal is HaddLe.
An exact proof term for the current goal is HaddLe2.
We use (open_ball X d x0 r) to witness the existential quantifier.
We will prove open_ball X d x0 r ∈ B0 ∧ (x0 ∈ open_ball X d x0 r ∧ open_ball X d x0 r ⊆ V).
Apply andI to the current goal.
We prove the intermediate claim HballIn: open_ball X d x0 r ∈ {open_ball X d x0 r0|r0 ∈ R, Rlt 0 r0}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d x0 r0) r HrR Hrpos).
An exact proof term for the current goal is (famunionI X (λx1 : set ⇒ {open_ball X d x1 r0|r0 ∈ R, Rlt 0 r0}) x0 (open_ball X d x0 r) Hx0X HballIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball X d x0 r Hd Hx0X Hrpos).
Let y0 be given.
Assume Hy0Ball: y0 ∈ open_ball X d x0 r.
We will prove y0 ∈ V.
We prove the intermediate claim Hy0X: y0 ∈ X.
An exact proof term for the current goal is (SepE1 X (λz0 : set ⇒ Rlt (apply_fun d (x0,z0)) r) y0 Hy0Ball).
We prove the intermediate claim Hdxy0: Rlt (apply_fun d (x0,y0)) r.
An exact proof term for the current goal is (SepE2 X (λz0 : set ⇒ Rlt (apply_fun d (x0,z0)) r) y0 Hy0Ball).
We prove the intermediate claim Hdxy0R: apply_fun d (x0,y0) ∈ R.
An exact proof term for the current goal is (metric_on_function_on X d Hd (x0,y0) (tuple_2_setprod_by_pair_Sigma X X x0 y0 Hx0X Hy0X)).
We prove the intermediate claim HleB: Rle (metric_dist_to_set X d y0 B) (add_SNo distB0 (apply_fun d (x0,y0))).
An exact proof term for the current goal is (metric_dist_to_set_Lipschitz X d x0 y0 B Hd Hx0X Hy0X HBsubX HBn).
We prove the intermediate claim HltB1: Rlt (add_SNo distB0 (apply_fun d (x0,y0))) (add_SNo distB0 r).
We prove the intermediate claim HdistB0S: SNo distB0.
An exact proof term for the current goal is (real_SNo distB0 HdistB0R).
We prove the intermediate claim Hdxy0S: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
An exact proof term for the current goal is (RltI (add_SNo distB0 (apply_fun d (x0,y0))) (add_SNo distB0 r) (real_add_SNo distB0 HdistB0R (apply_fun d (x0,y0)) Hdxy0R) (real_add_SNo distB0 HdistB0R r HrR) (add_SNo_Lt2 distB0 (apply_fun d (x0,y0)) r HdistB0S Hdxy0S HrS (RltE_lt (apply_fun d (x0,y0)) r Hdxy0))).
We prove the intermediate claim HltB: Rlt (metric_dist_to_set X d y0 B) (add_SNo distB0 r).
An exact proof term for the current goal is (Rle_Rlt_tra_Euclid (metric_dist_to_set X d y0 B) (add_SNo distB0 (apply_fun d (x0,y0))) (add_SNo distB0 r) HleB HltB1).
We prove the intermediate claim HleAswap: Rle distA0 (add_SNo (metric_dist_to_set X d y0 A) (apply_fun d (y0,x0))).
An exact proof term for the current goal is (metric_dist_to_set_Lipschitz X d y0 x0 A Hd Hy0X Hx0X HAsubX HAn).
We prove the intermediate claim Hsymd: apply_fun d (y0,x0) = apply_fun d (x0,y0).
An exact proof term for the current goal is (metric_on_symmetric X d y0 x0 Hd Hy0X Hx0X).
We prove the intermediate claim HleA: Rle distA0 (add_SNo (metric_dist_to_set X d y0 A) (apply_fun d (x0,y0))).
rewrite the current goal using Hsymd (from right to left).
An exact proof term for the current goal is HleAswap.
We prove the intermediate claim HlowerA: Rle (add_SNo distA0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 A).
We prove the intermediate claim HmdxyR: minus_SNo (apply_fun d (x0,y0)) ∈ R.
An exact proof term for the current goal is (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim Hshift: Rle (add_SNo (minus_SNo (apply_fun d (x0,y0))) distA0) (add_SNo (minus_SNo (apply_fun d (x0,y0))) (add_SNo (metric_dist_to_set X d y0 A) (apply_fun d (x0,y0)))).
An exact proof term for the current goal is (Rle_add_SNo_2 (minus_SNo (apply_fun d (x0,y0))) distA0 (add_SNo (metric_dist_to_set X d y0 A) (apply_fun d (x0,y0))) HmdxyR HdistA0R (real_add_SNo (metric_dist_to_set X d y0 A) (metric_dist_to_set_in_R X d y0 A Hd Hy0X HAsubX HAn) (apply_fun d (x0,y0)) Hdxy0R) HleA).
We prove the intermediate claim HlhsEq: add_SNo (minus_SNo (apply_fun d (x0,y0))) distA0 = add_SNo distA0 (minus_SNo (apply_fun d (x0,y0))).
An exact proof term for the current goal is (add_SNo_com (minus_SNo (apply_fun d (x0,y0))) distA0 (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) (real_SNo distA0 HdistA0R)).
We prove the intermediate claim HrhsEq: add_SNo (minus_SNo (apply_fun d (x0,y0))) (add_SNo (metric_dist_to_set X d y0 A) (apply_fun d (x0,y0))) = metric_dist_to_set X d y0 A.
We prove the intermediate claim HdxyS: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HA0R: metric_dist_to_set X d y0 A ∈ R.
An exact proof term for the current goal is (metric_dist_to_set_in_R X d y0 A Hd Hy0X HAsubX HAn).
We prove the intermediate claim HA0S: SNo (metric_dist_to_set X d y0 A).
An exact proof term for the current goal is (real_SNo (metric_dist_to_set X d y0 A) HA0R).
rewrite the current goal using (add_SNo_assoc (minus_SNo (apply_fun d (x0,y0))) (metric_dist_to_set X d y0 A) (apply_fun d (x0,y0)) (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) HA0S HdxyS) (from left to right).
rewrite the current goal using (add_SNo_com (minus_SNo (apply_fun d (x0,y0))) (metric_dist_to_set X d y0 A) (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) HA0S) (from left to right).
rewrite the current goal using (add_SNo_assoc (metric_dist_to_set X d y0 A) (minus_SNo (apply_fun d (x0,y0))) (apply_fun d (x0,y0)) HA0S (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) HdxyS) (from right to left).
rewrite the current goal using (add_SNo_minus_SNo_linv (apply_fun d (x0,y0)) HdxyS) (from left to right).
rewrite the current goal using (add_SNo_0R (metric_dist_to_set X d y0 A) HA0S) (from left to right).
Use reflexivity.
We prove the intermediate claim Hshift2: Rle (add_SNo distA0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 A).
rewrite the current goal using HlhsEq (from right to left).
rewrite the current goal using HrhsEq (from right to left).
An exact proof term for the current goal is Hshift.
An exact proof term for the current goal is Hshift2.
We prove the intermediate claim HltA0: Rlt (add_SNo distA0 (minus_SNo r)) (add_SNo distA0 (minus_SNo (apply_fun d (x0,y0)))).
We prove the intermediate claim HrS: SNo r.
An exact proof term for the current goal is (real_SNo r HrR).
We prove the intermediate claim HdxyS: SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x0,y0)) Hdxy0R).
We prove the intermediate claim HdxyLtS: apply_fun d (x0,y0) < r.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x0,y0)) r Hdxy0).
We prove the intermediate claim HnegLt: minus_SNo r < minus_SNo (apply_fun d (x0,y0)).
An exact proof term for the current goal is (minus_SNo_Lt_contra (apply_fun d (x0,y0)) r HdxyS HrS HdxyLtS).
An exact proof term for the current goal is (RltI (add_SNo distA0 (minus_SNo r)) (add_SNo distA0 (minus_SNo (apply_fun d (x0,y0)))) (real_add_SNo distA0 HdistA0R (minus_SNo r) (real_minus_SNo r HrR)) (real_add_SNo distA0 HdistA0R (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) (add_SNo_Lt2 distA0 (minus_SNo r) (minus_SNo (apply_fun d (x0,y0))) (real_SNo distA0 HdistA0R) (real_SNo (minus_SNo r) (real_minus_SNo r HrR)) (real_SNo (minus_SNo (apply_fun d (x0,y0))) (real_minus_SNo (apply_fun d (x0,y0)) Hdxy0R)) HnegLt)).
We prove the intermediate claim HltA: Rlt (add_SNo distA0 (minus_SNo r)) (metric_dist_to_set X d y0 A).
An exact proof term for the current goal is (Rlt_Rle_tra (add_SNo distA0 (minus_SNo r)) (add_SNo distA0 (minus_SNo (apply_fun d (x0,y0)))) (metric_dist_to_set X d y0 A) HltA0 HlowerA).
We prove the intermediate claim HltMid: Rlt (add_SNo distB0 r) (metric_dist_to_set X d y0 A).
An exact proof term for the current goal is (Rlt_tra (add_SNo distB0 r) (add_SNo distA0 (minus_SNo r)) (metric_dist_to_set X d y0 A) Hmargin HltA).
Apply (SepI X (λz0 : set ⇒ Rlt (metric_dist_to_set X d z0 B) (metric_dist_to_set X d z0 A)) y0 Hy0X) to the current goal.
An exact proof term for the current goal is (Rlt_tra (metric_dist_to_set X d y0 B) (add_SNo distB0 r) (metric_dist_to_set X d y0 A) HltB HltMid).
An exact proof term for the current goal is (SepI (𝒫 X) (λV0 : set ⇒ ∀x0 ∈ V0, ∃b ∈ B0, x0 ∈ b ∧ b ⊆ V0) V HVPow HVprop).
Let a be given.
Assume HaA: a ∈ A.
We will prove a ∈ U.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) B HBcl).
We prove the intermediate claim HaX: a ∈ X.
An exact proof term for the current goal is (HAsubX a HaA).
Apply (SepI X (λx0 : set ⇒ Rlt (metric_dist_to_set X d x0 A) (metric_dist_to_set X d x0 B)) a HaX) to the current goal.
We prove the intermediate claim HAne: A ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty A a HaA).
We prove the intermediate claim HBne: B ≠ Empty.
An exact proof term for the current goal is HBn.
We prove the intermediate claim Ha_notB: a ∉ B.
Assume HaB: a ∈ B.
We prove the intermediate claim HaAB: a ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B a HaA HaB).
We prove the intermediate claim HaE: a ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HaAB.
An exact proof term for the current goal is (EmptyE a HaE False).
We prove the intermediate claim HdistA0: metric_dist_to_set X d a A = 0.
An exact proof term for the current goal is (metric_dist_to_set_eq_0_if_mem X d a A Hd HaX HAsubX HaA).
We prove the intermediate claim HdistBpos: Rlt 0 (metric_dist_to_set X d a B).
An exact proof term for the current goal is (metric_dist_to_closed_set_pos_if_not_mem X d B a Hd HBcl HaX Ha_notB HBne).
rewrite the current goal using HdistA0 (from left to right).
An exact proof term for the current goal is HdistBpos.
Let b be given.
Assume HbB: b ∈ B.
We will prove b ∈ V.
We prove the intermediate claim HAsubX: A ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) A HAcl).
We prove the intermediate claim HBsubX: B ⊆ X.
An exact proof term for the current goal is (closed_in_subset X (metric_topology X d) B HBcl).
We prove the intermediate claim HbX: b ∈ X.
An exact proof term for the current goal is (HBsubX b HbB).
Apply (SepI X (λx0 : set ⇒ Rlt (metric_dist_to_set X d x0 B) (metric_dist_to_set X d x0 A)) b HbX) to the current goal.
We prove the intermediate claim HAne: A ≠ Empty.
An exact proof term for the current goal is HAn.
We prove the intermediate claim HBne: B ≠ Empty.
An exact proof term for the current goal is (elem_implies_nonempty B b HbB).
We prove the intermediate claim Hb_notA: b ∉ A.
Assume HbA: b ∈ A.
We prove the intermediate claim HbAB: b ∈ A ∩ B.
An exact proof term for the current goal is (binintersectI A B b HbA HbB).
We prove the intermediate claim HbE: b ∈ Empty.
rewrite the current goal using Hdisj (from right to left).
An exact proof term for the current goal is HbAB.
An exact proof term for the current goal is (EmptyE b HbE False).
We prove the intermediate claim HdistB0: metric_dist_to_set X d b B = 0.
An exact proof term for the current goal is (metric_dist_to_set_eq_0_if_mem X d b B Hd HbX HBsubX HbB).
We prove the intermediate claim HdistApos: Rlt 0 (metric_dist_to_set X d b A).
An exact proof term for the current goal is (metric_dist_to_closed_set_pos_if_not_mem X d A b Hd HAcl HbX Hb_notA HAne).
rewrite the current goal using HdistB0 (from left to right).
An exact proof term for the current goal is HdistApos.
Apply set_ext to the current goal.
Let x be given.
Assume Hx: x ∈ U ∩ V.
We will prove x ∈ Empty.
We prove the intermediate claim HxU: x ∈ U.
An exact proof term for the current goal is (binintersectE1 U V x Hx).
We prove the intermediate claim HxV: x ∈ V.
An exact proof term for the current goal is (binintersectE2 U V x Hx).
We prove the intermediate claim HltAB: Rlt (metric_dist_to_set X d x A) (metric_dist_to_set X d x B).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ Rlt (metric_dist_to_set X d x0 A) (metric_dist_to_set X d x0 B)) x HxU).
We prove the intermediate claim HltBA: Rlt (metric_dist_to_set X d x B) (metric_dist_to_set X d x A).
An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ Rlt (metric_dist_to_set X d x0 B) (metric_dist_to_set X d x0 A)) x HxV).
Apply FalseE to the current goal.
An exact proof term for the current goal is ((not_Rlt_sym (metric_dist_to_set X d x A) (metric_dist_to_set X d x B) HltAB) HltBA).
Let x be given.
Assume Hx: x ∈ Empty.
We will prove x ∈ U ∩ V.
An exact proof term for the current goal is (EmptyE x Hx (x ∈ U ∩ V)).
∎