Let X and d be given.
Assume Hm: metric_on X d.
We will prove Hausdorff_space X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀x1 x2 : set, x1 ∈ X → x2 ∈ X → x1 ≠ x2 → ∃U V : set, U ∈ metric_topology X d ∧ V ∈ metric_topology X d ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
Let x1 and x2 be given.
Assume Hx1X: x1 ∈ X.
Assume Hx2X: x2 ∈ X.
Assume Hneq: x1 ≠ x2.
We will prove ∃U V : set, U ∈ metric_topology X d ∧ V ∈ metric_topology X d ∧ x1 ∈ U ∧ x2 ∈ V ∧ U ∩ V = Empty.
We prove the intermediate claim Hdistpos: Rlt 0 (apply_fun d (x1,x2)).
An exact proof term for the current goal is (metric_on_pos_of_neq X d x1 x2 Hm Hx1X Hx2X Hneq).
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 Hx1x2In: (x1,x2) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x1 x2 Hx1X Hx2X).
We prove the intermediate claim HdistR: apply_fun d (x1,x2) ∈ R.
An exact proof term for the current goal is (Hfun (x1,x2) Hx1x2In).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < apply_fun d (x1,x2).
An exact proof term for the current goal is (exists_eps_lt_pos (apply_fun d (x1,x2)) HdistR Hdistpos).
Apply HexN to the current goal.
Let N be given.
Assume HNpair.
We prove the intermediate claim HNomega: N ∈ ω.
An exact proof term for the current goal is (andEL (N ∈ ω) (eps_ N < apply_fun d (x1,x2)) HNpair).
We prove the intermediate claim HepsNlt: eps_ N < apply_fun d (x1,x2).
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < apply_fun d (x1,x2)) HNpair).
We prove the intermediate claim HsuccOmega: ordsucc N ∈ ω.
An exact proof term for the current goal is (omega_ordsucc N HNomega).
Set r to be the term eps_ (ordsucc N).
We prove the intermediate claim Hrdef: r = eps_ (ordsucc N).
Use reflexivity.
We prove the intermediate claim HrR: r ∈ R.
rewrite the current goal using Hrdef (from left to right).
An exact proof term for the current goal is (SNoS_omega_real (eps_ (ordsucc N)) (SNo_eps_SNoS_omega (ordsucc N) HsuccOmega)).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (RltI 0 r real_0 HrR (SNo_eps_pos (ordsucc N) HsuccOmega)).
Set U to be the term open_ball X d x1 r.
Set V to be the term open_ball X d x2 r.
We prove the intermediate claim HUopen: U ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x1 r Hm Hx1X Hrpos).
We prove the intermediate claim HVopen: V ∈ metric_topology X d.
An exact proof term for the current goal is (open_ball_in_metric_topology X d x2 r Hm Hx2X Hrpos).
We prove the intermediate claim Hx1U: x1 ∈ U.
An exact proof term for the current goal is (center_in_open_ball X d x1 r Hm Hx1X Hrpos).
We prove the intermediate claim Hx2V: x2 ∈ V.
An exact proof term for the current goal is (center_in_open_ball X d x2 r Hm Hx2X Hrpos).
We prove the intermediate claim HUVdisj: U ∩ V = Empty.
Apply Empty_Subq_eq to the current goal.
Let z be given.
Assume Hz: z ∈ U ∩ V.
We will prove z ∈ Empty.
Apply FalseE to the current goal.
We prove the intermediate claim HzU: z ∈ U.
An exact proof term for the current goal is (binintersectE1 U V z Hz).
We prove the intermediate claim HzV: z ∈ V.
An exact proof term for the current goal is (binintersectE2 U V z Hz).
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x1 r z HzU).
We prove the intermediate claim Hxz1: Rlt (apply_fun d (x1,z)) r.
An exact proof term for the current goal is (open_ballE2 X d x1 r z HzU).
We prove the intermediate claim Hxz2raw: Rlt (apply_fun d (x2,z)) r.
An exact proof term for the current goal is (open_ballE2 X d x2 r z HzV).
We prove the intermediate claim Hsym: apply_fun d (z,x2) = apply_fun d (x2,z).
An exact proof term for the current goal is (metric_on_symmetric X d z x2 Hm HzX Hx2X).
We prove the intermediate claim Hxz2: Rlt (apply_fun d (z,x2)) r.
rewrite the current goal using Hsym (from left to right).
An exact proof term for the current goal is Hxz2raw.
We prove the intermediate claim Hx1zIn: (x1,z) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X x1 z Hx1X HzX).
We prove the intermediate claim Hzx2In: (z,x2) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X z x2 HzX Hx2X).
We prove the intermediate claim Hd1R: apply_fun d (x1,z) ∈ R.
An exact proof term for the current goal is (Hfun (x1,z) Hx1zIn).
We prove the intermediate claim Hd2R: apply_fun d (z,x2) ∈ R.
An exact proof term for the current goal is (Hfun (z,x2) Hzx2In).
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 Hd1S: SNo (apply_fun d (x1,z)).
An exact proof term for the current goal is (real_SNo (apply_fun d (x1,z)) Hd1R).
We prove the intermediate claim Hd2S: SNo (apply_fun d (z,x2)).
An exact proof term for the current goal is (real_SNo (apply_fun d (z,x2)) Hd2R).
We prove the intermediate claim Hd1lt: apply_fun d (x1,z) < r.
An exact proof term for the current goal is (RltE_lt (apply_fun d (x1,z)) r Hxz1).
We prove the intermediate claim Hd2lt: apply_fun d (z,x2) < r.
An exact proof term for the current goal is (RltE_lt (apply_fun d (z,x2)) r Hxz2).
We prove the intermediate claim Hsumlt: add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2)) < add_SNo r r.
An exact proof term for the current goal is (add_SNo_Lt3 (apply_fun d (x1,z)) (apply_fun d (z,x2)) r r Hd1S Hd2S HrS HrS Hd1lt Hd2lt).
We prove the intermediate claim HsumR: add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2)) ∈ R.
An exact proof term for the current goal is (real_add_SNo (apply_fun d (x1,z)) Hd1R (apply_fun d (z,x2)) Hd2R).
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 HsumRlt_rr: Rlt (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))) (add_SNo r r).
An exact proof term for the current goal is (RltI (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))) (add_SNo r r) HsumR HrrR Hsumlt).
We prove the intermediate claim HNnat: nat_p N.
An exact proof term for the current goal is (omega_nat_p N HNomega).
We prove the intermediate claim HrrEq: add_SNo r r = eps_ N.
rewrite the current goal using (eps_ordsucc_half_add N HNnat) (from left to right).
Use reflexivity.
We prove the intermediate claim HepsNR: eps_ N ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)).
We prove the intermediate claim Hrrlt: Rlt (add_SNo r r) (apply_fun d (x1,x2)).
rewrite the current goal using HrrEq (from left to right).
An exact proof term for the current goal is (RltI (eps_ N) (apply_fun d (x1,x2)) HepsNR HdistR HepsNlt).
We prove the intermediate claim HsumRlt_dist: Rlt (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))) (apply_fun d (x1,x2)).
An exact proof term for the current goal is (Rlt_tra (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))) (add_SNo r r) (apply_fun d (x1,x2)) HsumRlt_rr Hrrlt).
We prove the intermediate claim Htri: Rle (apply_fun d (x1,x2)) (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))).
An exact proof term for the current goal is (metric_triangle_Rle X d x1 z x2 Hm Hx1X HzX Hx2X).
An exact proof term for the current goal is ((RleE_nlt (apply_fun d (x1,x2)) (add_SNo (apply_fun d (x1,z)) (apply_fun d (z,x2))) Htri) HsumRlt_dist).
We use U to witness the existential quantifier.
We use V to witness the existential quantifier.
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 HUopen.
An exact proof term for the current goal is HVopen.
An exact proof term for the current goal is Hx1U.
An exact proof term for the current goal is Hx2V.
An exact proof term for the current goal is HUVdisj.
∎