Let X and d be given.
Assume Hm: metric_on X d.
We will prove one_point_sets_closed X (metric_topology X d).
We will prove topology_on X (metric_topology X d) ∧ ∀x : set, x ∈ X → closed_in X (metric_topology X d) {x}.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_topology_is_topology X d Hm).
Let x be given.
Assume HxX: x ∈ X.
We will prove closed_in X (metric_topology X d) {x}.
Set U to be the term X ∖ {x}.
We prove the intermediate claim HsingSub: {x} ⊆ X.
An exact proof term for the current goal is (singleton_subset x X HxX).
We prove the intermediate claim HUsub: U ⊆ X.
Apply setminus_Subq to the current goal.
We prove the intermediate claim HUopen: U ∈ metric_topology X d.
Set B to be the term famunion X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}).
We prove the intermediate claim HUbasis: U ∈ generated_topology X B.
We prove the intermediate claim HUprop: ∀y ∈ U, ∃b ∈ B, y ∈ b ∧ b ⊆ U.
Let y be given.
Assume HyU: y ∈ U.
We will prove ∃b ∈ B, y ∈ b ∧ b ⊆ U.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (setminusE1 X {x} y HyU).
We prove the intermediate claim Hynot: y ∉ {x}.
An exact proof term for the current goal is (setminusE2 X {x} y HyU).
We prove the intermediate claim Hneq: ¬ (y = x).
Assume Heq: y = x.
Apply Hynot to the current goal.
rewrite the current goal using Heq (from left to right).
An exact proof term for the current goal is (SingI x).
We prove the intermediate claim Hrpos: Rlt 0 (apply_fun d (y,x)).
An exact proof term for the current goal is (metric_on_pos_of_neq X d y x Hm HyX HxX Hneq).
We use (open_ball X d y (apply_fun d (y,x))) to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HrR: apply_fun d (y,x) ∈ R.
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 HyxIn: (y,x) ∈ setprod X X.
An exact proof term for the current goal is (tuple_2_setprod_by_pair_Sigma X X y x HyX HxX).
An exact proof term for the current goal is (Hfun (y,x) HyxIn).
We prove the intermediate claim HballIn: open_ball X d y (apply_fun d (y,x)) ∈ {open_ball X d y r|r ∈ R, Rlt 0 r}.
An exact proof term for the current goal is (ReplSepI R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d y r0) (apply_fun d (y,x)) HrR Hrpos).
An exact proof term for the current goal is (famunionI X (λx0 : set ⇒ {open_ball X d x0 r|r ∈ R, Rlt 0 r}) y (open_ball X d y (apply_fun d (y,x))) HyX HballIn).
Apply andI to the current goal.
An exact proof term for the current goal is (center_in_open_ball X d y (apply_fun d (y,x)) Hm HyX Hrpos).
Let z be given.
Assume Hz: z ∈ open_ball X d y (apply_fun d (y,x)).
We will prove z ∈ U.
We prove the intermediate claim HzX: z ∈ X.
An exact proof term for the current goal is (open_ballE1 X d y (apply_fun d (y,x)) z Hz).
We prove the intermediate claim Hznotsing: z ∉ {x}.
Assume Hzsing: z ∈ {x}.
We prove the intermediate claim Hzeq: z = x.
An exact proof term for the current goal is (SingE x z Hzsing).
We prove the intermediate claim Hxball: x ∈ open_ball X d y (apply_fun d (y,x)).
rewrite the current goal using Hzeq (from right to left) at position 1.
An exact proof term for the current goal is Hz.
We prove the intermediate claim Hlt: Rlt (apply_fun d (y,x)) (apply_fun d (y,x)).
An exact proof term for the current goal is (open_ballE2 X d y (apply_fun d (y,x)) x Hxball).
Apply FalseE to the current goal.
An exact proof term for the current goal is ((not_Rlt_refl (apply_fun d (y,x)) (RltE_right 0 (apply_fun d (y,x)) Hrpos)) Hlt).
An exact proof term for the current goal is (setminusI X {x} z HzX Hznotsing).
An exact proof term for the current goal is (SepI (𝒫 X) (λU0 : set ⇒ ∀y ∈ U0, ∃b ∈ B, y ∈ b ∧ b ⊆ U0) U (PowerI X U HUsub) HUprop).
rewrite the current goal using (metric_topology_generated_by_balls X d Hm) (from right to left).
An exact proof term for the current goal is HUbasis.
We prove the intermediate claim HclosedComp: closed_in X (metric_topology X d) (X ∖ U).
An exact proof term for the current goal is (closed_of_open_complement X (metric_topology X d) U (metric_topology_is_topology X d Hm) HUopen).
We prove the intermediate claim Heq: X ∖ U = {x}.
We prove the intermediate claim HUdef: U = X ∖ {x}.
Use reflexivity.
rewrite the current goal using HUdef (from left to right).
An exact proof term for the current goal is (setminus_setminus_eq X {x} HsingSub).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is HclosedComp.
∎