Apply andI to the current goal.

We prove the intermediate claim Homega_countable: countable ω.

An exact proof term for the current goal is (Subq_atleastp ω ω (Subq_ref ω)).

We prove the intermediate claim HFamDef: Fam = {⋃ {open_ball X d a (eps_ n)|a ∈ A}|n ∈ ω}.

Use reflexivity.

rewrite the current goal using HFamDef (from left to right).

An exact proof term for the current goal is (countable_image ω Homega_countable (λn : set ⇒ ⋃ {open_ball X d a (eps_ n)|a ∈ A})).

Let U be given.

Assume HU: U ∈ Fam.

We will prove open_in X Tx U.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (metric_topology_is_topology X d Hm).

Apply (open_inI X Tx U HTx) to the current goal.

We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ U = ⋃ {open_ball X d a (eps_ n)|a ∈ A}.

An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ ⋃ {open_ball X d a (eps_ n0)|a ∈ A}) U HU).

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 ∈ ω) (U = ⋃ {open_ball X d a (eps_ n)|a ∈ A}) Hnpair).

We prove the intermediate claim HUeq: U = ⋃ {open_ball X d a (eps_ n)|a ∈ A}.

An exact proof term for the current goal is (andER (n ∈ ω) (U = ⋃ {open_ball X d a (eps_ n)|a ∈ A}) Hnpair).

rewrite the current goal using HUeq (from left to right).

Set BallFam to be the term {open_ball X d a (eps_ n)|a ∈ A}.

We prove the intermediate claim HBallSub: BallFam ⊆ Tx.

Let b be given.

Assume Hb: b ∈ BallFam.

We will prove b ∈ Tx.

Apply (ReplE_impred A (λa0 : set ⇒ open_ball X d a0 (eps_ n)) b Hb (b ∈ Tx)) to the current goal.

Let a0 be given.

Assume Ha0A.

Assume Hbeq: b = open_ball X d a0 (eps_ n).

rewrite the current goal using Hbeq (from left to right).

We prove the intermediate claim HAsubX: A ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).

We prove the intermediate claim Ha0X: a0 ∈ X.

An exact proof term for the current goal is (HAsubX a0 Ha0A).

We prove the intermediate claim HepsInS: eps_ n ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega n Hnomega).

We prove the intermediate claim HepsR: eps_ n ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ n) HepsInS).

We prove the intermediate claim HepsposS: 0 < (eps_ n).

An exact proof term for the current goal is (SNo_eps_pos n Hnomega).

We prove the intermediate claim Hepspos: Rlt 0 (eps_ n).

An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsR HepsposS).

An exact proof term for the current goal is (open_ball_in_metric_topology X d a0 (eps_ n) Hm Ha0X Hepspos).

We prove the intermediate claim HUnionIn: ⋃ BallFam ∈ Tx.

An exact proof term for the current goal is (topology_union_closed X Tx BallFam HTx HBallSub).

We prove the intermediate claim HUnionEq: ⋃ BallFam = ⋃ {open_ball X d a (eps_ n)|a ∈ A}.

Use reflexivity.

rewrite the current goal using HUnionEq (from right to left).

An exact proof term for the current goal is HUnionIn.

Apply set_ext to the current goal.

Let x be given.

Assume HxInt: x ∈ intersection_over_family X Fam.

We will prove x ∈ A.

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (SepE1 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxInt).

We prove the intermediate claim HallU: ∀U0 : set, U0 ∈ Fam → x ∈ U0.

An exact proof term for the current goal is (SepE2 X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxInt).

Apply (xm (x ∈ A)) to the current goal.

Assume HxA: x ∈ A.

An exact proof term for the current goal is HxA.

Assume HxNotA: ¬ (x ∈ A).

Apply FalseE to the current goal.

We prove the intermediate claim HcompOpen: open_in X Tx (X ∖ A).

An exact proof term for the current goal is (open_of_closed_complement X Tx A HAcl).

We prove the intermediate claim HxComp: x ∈ X ∖ A.

An exact proof term for the current goal is (setminusI X A x HxX HxNotA).

We prove the intermediate claim HcompInT: (X ∖ A) ∈ Tx.

An exact proof term for the current goal is (open_in_elem X Tx (X ∖ A) HcompOpen).

Set B to be the term famunion X (λc : set ⇒ {open_ball X d c r|r ∈ R, Rlt 0 r}).

We prove the intermediate claim HTdef: Tx = generated_topology X B.

Use reflexivity.

We prove the intermediate claim Hgen: generated_topology X B = {U0 ∈ 𝒫 X|∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0}.

Use reflexivity.

We prove the intermediate claim HcompInGen: (X ∖ A) ∈ generated_topology X B.

rewrite the current goal using HTdef (from right to left).

An exact proof term for the current goal is HcompInT.

We prove the intermediate claim HcompMem: (X ∖ A) ∈ {U0 ∈ 𝒫 X|∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0}.

rewrite the current goal using Hgen (from right to left).

An exact proof term for the current goal is HcompInGen.

We prove the intermediate claim HcompProp: ∀y0 ∈ (X ∖ A), ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ (X ∖ A).

An exact proof term for the current goal is (SepE2 (𝒫 X) (λU0 : set ⇒ ∀y0 ∈ U0, ∃b0 ∈ B, y0 ∈ b0 ∧ b0 ⊆ U0) (X ∖ A) HcompMem).

We prove the intermediate claim Hexb: ∃b : set, b ∈ B ∧ (x ∈ b ∧ b ⊆ (X ∖ A)).

An exact proof term for the current goal is (HcompProp x HxComp).

Apply Hexb to the current goal.

Let b be given.

Assume Hbpack.

We prove the intermediate claim HbB: b ∈ B.

An exact proof term for the current goal is (andEL (b ∈ B) (x ∈ b ∧ b ⊆ (X ∖ A)) Hbpack).

We prove the intermediate claim Hbrest: x ∈ b ∧ b ⊆ (X ∖ A).

An exact proof term for the current goal is (andER (b ∈ B) (x ∈ b ∧ b ⊆ (X ∖ A)) Hbpack).

We prove the intermediate claim Hxb: x ∈ b.

An exact proof term for the current goal is (andEL (x ∈ b) (b ⊆ (X ∖ A)) Hbrest).

We prove the intermediate claim HbSubComp: b ⊆ (X ∖ A).

An exact proof term for the current goal is (andER (x ∈ b) (b ⊆ (X ∖ A)) Hbrest).

We prove the intermediate claim Hexc: ∃c : set, c ∈ X ∧ b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.

Apply (famunionE_impred X (λc0 : set ⇒ {open_ball X d c0 r|r ∈ R, Rlt 0 r}) b HbB (∃c : set, c ∈ X ∧ b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r})) to the current goal.

Let c0 be given.

Assume Hc0X.

Assume HbIn: b ∈ {open_ball X d c0 r|r ∈ R, Rlt 0 r}.

We use c0 to witness the existential quantifier.

An exact proof term for the current goal is (andI (c0 ∈ X) (b ∈ {open_ball X d c0 r|r ∈ R, Rlt 0 r}) Hc0X HbIn).

Apply Hexc to the current goal.

Let c be given.

Assume Hcpack.

We prove the intermediate claim HcX: c ∈ X.

An exact proof term for the current goal is (andEL (c ∈ X) (b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}) Hcpack).

We prove the intermediate claim HbInC: b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}.

An exact proof term for the current goal is (andER (c ∈ X) (b ∈ {open_ball X d c r|r ∈ R, Rlt 0 r}) Hcpack).

We prove the intermediate claim Hexr: ∃r0 : set, r0 ∈ R ∧ (Rlt 0 r0 ∧ b = open_ball X d c r0).

Apply (ReplSepE_impred R (λr0 : set ⇒ Rlt 0 r0) (λr0 : set ⇒ open_ball X d c r0) b HbInC (∃r0 : set, r0 ∈ R ∧ (Rlt 0 r0 ∧ b = open_ball X d c r0))) to the current goal.

Let r0 be given.

Assume Hr0R: r0 ∈ R.

Assume Hr0pos: Rlt 0 r0.

Assume Hbeq: b = open_ball X d c r0.

We use r0 to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hr0R.

Apply andI to the current goal.

An exact proof term for the current goal is Hr0pos.

An exact proof term for the current goal is Hbeq.

Apply Hexr to the current goal.

Let r0 be given.

Assume Hrpack.

We prove the intermediate claim Hr0R: r0 ∈ R.

An exact proof term for the current goal is (andEL (r0 ∈ R) (Rlt 0 r0 ∧ b = open_ball X d c r0) Hrpack).

We prove the intermediate claim Hrrest: Rlt 0 r0 ∧ b = open_ball X d c r0.

An exact proof term for the current goal is (andER (r0 ∈ R) (Rlt 0 r0 ∧ b = open_ball X d c r0) Hrpack).

We prove the intermediate claim Hr0pos: Rlt 0 r0.

An exact proof term for the current goal is (andEL (Rlt 0 r0) (b = open_ball X d c r0) Hrrest).

We prove the intermediate claim Hbeq: b = open_ball X d c r0.

An exact proof term for the current goal is (andER (Rlt 0 r0) (b = open_ball X d c r0) Hrrest).

We prove the intermediate claim HxinBall: x ∈ open_ball X d c r0.

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is Hxb.

We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r0.

An exact proof term for the current goal is (open_ball_refine_center X d c x r0 Hm HcX HxX Hr0R Hr0pos HxinBall).

Apply Hexs to the current goal.

Let s be given.

Assume Hspack.

We prove the intermediate claim HsRpos: s ∈ R ∧ Rlt 0 s.

An exact proof term for the current goal is (andEL (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hspack).

We prove the intermediate claim HsR: s ∈ R.

An exact proof term for the current goal is (andEL (s ∈ R) (Rlt 0 s) HsRpos).

We prove the intermediate claim Hspos: Rlt 0 s.

An exact proof term for the current goal is (andER (s ∈ R) (Rlt 0 s) HsRpos).

We prove the intermediate claim HsubBall: open_ball X d x s ⊆ open_ball X d c r0.

An exact proof term for the current goal is (andER (s ∈ R ∧ Rlt 0 s) (open_ball X d x s ⊆ open_ball X d c r0) Hspack).

We prove the intermediate claim HballSubComp: open_ball X d x s ⊆ (X ∖ A).

We prove the intermediate claim HbBallSubComp: open_ball X d c r0 ⊆ (X ∖ A).

rewrite the current goal using Hbeq (from right to left).

An exact proof term for the current goal is HbSubComp.

An exact proof term for the current goal is (Subq_tra (open_ball X d x s) (open_ball X d c r0) (X ∖ A) HsubBall HbBallSubComp).

We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < s.

An exact proof term for the current goal is (exists_eps_lt_pos_Euclid s HsR Hspos).

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 < s) HNpair).

We prove the intermediate claim HepsLtS: eps_ N < s.

An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < s) HNpair).

Set UN to be the term ⋃ {open_ball X d a (eps_ N)|a ∈ A}.

We prove the intermediate claim HUNinFam: UN ∈ Fam.

An exact proof term for the current goal is (ReplI ω (λn0 : set ⇒ ⋃ {open_ball X d a (eps_ n0)|a ∈ A}) N HNomega).

We prove the intermediate claim HxUN: x ∈ UN.

An exact proof term for the current goal is (HallU UN HUNinFam).

Apply (UnionE_impred {open_ball X d a (eps_ N)|a ∈ A} x HxUN False) to the current goal.

Let V be given.

Assume HxV: x ∈ V.

Assume HV: V ∈ {open_ball X d a (eps_ N)|a ∈ A}.

We prove the intermediate claim Hexa: ∃a : set, a ∈ A ∧ V = open_ball X d a (eps_ N).

An exact proof term for the current goal is (ReplE A (λa0 : set ⇒ open_ball X d a0 (eps_ N)) V HV).

Apply Hexa to the current goal.

Let a0 be given.

Assume Ha0pack.

We prove the intermediate claim Ha0A: a0 ∈ A.

An exact proof term for the current goal is (andEL (a0 ∈ A) (V = open_ball X d a0 (eps_ N)) Ha0pack).

We prove the intermediate claim HVeq: V = open_ball X d a0 (eps_ N).

An exact proof term for the current goal is (andER (a0 ∈ A) (V = open_ball X d a0 (eps_ N)) Ha0pack).

We prove the intermediate claim HAsubX: A ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).

We prove the intermediate claim Ha0X: a0 ∈ X.

An exact proof term for the current goal is (HAsubX a0 Ha0A).

We prove the intermediate claim HxInBallA: x ∈ open_ball X d a0 (eps_ N).

rewrite the current goal using HVeq (from right to left).

An exact proof term for the current goal is HxV.

We prove the intermediate claim HltA: Rlt (apply_fun d (a0,x)) (eps_ N).

An exact proof term for the current goal is (open_ballE2 X d a0 (eps_ N) x HxInBallA).

We prove the intermediate claim Hsym: apply_fun d (a0,x) = apply_fun d (x,a0).

An exact proof term for the current goal is (metric_on_symmetric X d a0 x Hm Ha0X HxX).

We prove the intermediate claim HltX: Rlt (apply_fun d (x,a0)) (eps_ N).

rewrite the current goal using Hsym (from right to left).

An exact proof term for the current goal is HltA.

We prove the intermediate claim Ha0InBallX: a0 ∈ open_ball X d x (eps_ N).

An exact proof term for the current goal is (open_ballI X d x (eps_ N) a0 Ha0X HltX).

We prove the intermediate claim HballMono: open_ball X d x (eps_ N) ⊆ open_ball X d x s.

We prove the intermediate claim HltEps: Rlt (eps_ N) s.

An exact proof term for the current goal is (RltI (eps_ N) s (SNoS_omega_real (eps_ N) (SNo_eps_SNoS_omega N HNomega)) HsR HepsLtS).

An exact proof term for the current goal is (open_ball_radius_mono X d x (eps_ N) s HltEps).

We prove the intermediate claim Ha0InBallS: a0 ∈ open_ball X d x s.

An exact proof term for the current goal is (HballMono a0 Ha0InBallX).

We prove the intermediate claim Ha0NotA: a0 ∉ A.

Assume Ha0inA: a0 ∈ A.

We prove the intermediate claim Ha0inComp: a0 ∈ X ∖ A.

An exact proof term for the current goal is (HballSubComp a0 Ha0InBallS).

We prove the intermediate claim Ha0notA': a0 ∉ A.

An exact proof term for the current goal is (setminusE2 X A a0 Ha0inComp).

An exact proof term for the current goal is (Ha0notA' Ha0inA).

An exact proof term for the current goal is (Ha0NotA Ha0A).

Let x be given.

Assume HxA: x ∈ A.

We will prove x ∈ intersection_over_family X Fam.

We prove the intermediate claim HAsubX: A ⊆ X.

An exact proof term for the current goal is (closed_in_subset X Tx A HAcl).

We prove the intermediate claim HxX: x ∈ X.

An exact proof term for the current goal is (HAsubX x HxA).

We prove the intermediate claim HIntDef: intersection_over_family X Fam = {x0 ∈ X|∀U0 : set, U0 ∈ Fam → x0 ∈ U0}.

Use reflexivity.

rewrite the current goal using HIntDef (from left to right).

Apply (SepI X (λx0 : set ⇒ ∀U0 : set, U0 ∈ Fam → x0 ∈ U0) x HxX) to the current goal.

Let U0 be given.

Assume HU0: U0 ∈ Fam.

We prove the intermediate claim Hexn: ∃n : set, n ∈ ω ∧ U0 = ⋃ {open_ball X d a (eps_ n)|a ∈ A}.

An exact proof term for the current goal is (ReplE ω (λn0 : set ⇒ ⋃ {open_ball X d a (eps_ n0)|a ∈ A}) U0 HU0).

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 ∈ ω) (U0 = ⋃ {open_ball X d a (eps_ n)|a ∈ A}) Hnpair).

We prove the intermediate claim HU0eq: U0 = ⋃ {open_ball X d a (eps_ n)|a ∈ A}.

An exact proof term for the current goal is (andER (n ∈ ω) (U0 = ⋃ {open_ball X d a (eps_ n)|a ∈ A}) Hnpair).

rewrite the current goal using HU0eq (from left to right).

We prove the intermediate claim HepsInS: eps_ n ∈ SNoS_ ω.

An exact proof term for the current goal is (SNo_eps_SNoS_omega n Hnomega).

We prove the intermediate claim HepsR: eps_ n ∈ R.

An exact proof term for the current goal is (SNoS_omega_real (eps_ n) HepsInS).

We prove the intermediate claim HepsposS: 0 < (eps_ n).

An exact proof term for the current goal is (SNo_eps_pos n Hnomega).

We prove the intermediate claim Hepspos: Rlt 0 (eps_ n).

An exact proof term for the current goal is (RltI 0 (eps_ n) real_0 HepsR HepsposS).

We prove the intermediate claim Hdxx0: apply_fun d (x,x) = 0.

An exact proof term for the current goal is (metric_on_diag_zero X d x Hm HxX).

We prove the intermediate claim Hlt: Rlt (apply_fun d (x,x)) (eps_ n).

rewrite the current goal using Hdxx0 (from left to right).

An exact proof term for the current goal is Hepspos.

We prove the intermediate claim HxBall: x ∈ open_ball X d x (eps_ n).

An exact proof term for the current goal is (open_ballI X d x (eps_ n) x HxX Hlt).

We prove the intermediate claim HballInFam: open_ball X d x (eps_ n) ∈ {open_ball X d a (eps_ n)|a ∈ A}.

An exact proof term for the current goal is (ReplI A (λa0 : set ⇒ open_ball X d a0 (eps_ n)) x HxA).

An exact proof term for the current goal is (UnionI {open_ball X d a (eps_ n)|a ∈ A} x (open_ball X d x (eps_ n)) HxBall HballInFam).