Let X, d, S and n be given.
Assume Hm: metric_on X d.
Assume HnO: n ∈ ω.
Assume Hsep: eps_separated_set X d S n.
Set Tx to be the term metric_topology X d.
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).
We will prove locally_finite_family X Tx {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
We will prove topology_on X Tx ∧ ∀p : set, p ∈ X → ∃N : set, N ∈ Tx ∧ p ∈ N ∧ ∃SF : set, finite SF ∧ SF ⊆ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S} ∧ ∀A : set, A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S} → A ∩ N ≠ Empty → A ∈ SF.
Apply andI to the current goal.
An exact proof term for the current goal is HTx.
Let p be given.
Assume HpX: p ∈ X.
Set r to be the term eps_ (ordsucc (ordsucc n)).
We prove the intermediate claim Hsucc1: ordsucc n ∈ ω.
An exact proof term for the current goal is (omega_ordsucc n HnO).
We prove the intermediate claim Hsucc2: ordsucc (ordsucc n) ∈ ω.
An exact proof term for the current goal is (omega_ordsucc (ordsucc n) Hsucc1).
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 (ordsucc n)) Hsucc2)).
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 (ordsucc n)) Hsucc2)).
Set N to be the term open_ball X d p r.
We use N 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 (open_ball_in_metric_topology X d p r Hm HpX HrPos).
An exact proof term for the current goal is (center_in_open_ball X d p r Hm HpX HrPos).
Apply (xm (∃A : set, A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S} ∧ A ∩ N ≠ Empty)) to the current goal.
Assume HexA.
Apply HexA to the current goal.
Let A0 be given.
Assume HA0pack.
We prove the intermediate claim HA0inF: A0 ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
An exact proof term for the current goal is (andEL (A0 ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}) (A0 ∩ N ≠ Empty) HA0pack).
We prove the intermediate claim HA0meet: A0 ∩ N ≠ Empty.
An exact proof term for the current goal is (andER (A0 ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}) (A0 ∩ N ≠ Empty) HA0pack).
Apply (ReplE S (λx : set ⇒ open_ball X d x r) A0 HA0inF) to the current goal.
Let x0 be given.
Assume Hx0pack.
We prove the intermediate claim Hx0S: x0 ∈ S.
An exact proof term for the current goal is (andEL (x0 ∈ S) (A0 = open_ball X d x0 r) Hx0pack).
We prove the intermediate claim HA0eq: A0 = open_ball X d x0 r.
An exact proof term for the current goal is (andER (x0 ∈ S) (A0 = open_ball X d x0 r) Hx0pack).
We prove the intermediate claim Hexq0: ∃q0 : set, q0 ∈ (A0 ∩ N).
An exact proof term for the current goal is (nonempty_has_element (A0 ∩ N) HA0meet).
Apply Hexq0 to the current goal.
Let q0 be given.
Assume Hq0in.
We prove the intermediate claim Hq0AN: q0 ∈ A0 ∧ q0 ∈ N.
An exact proof term for the current goal is (binintersectE A0 N q0 Hq0in).
We prove the intermediate claim Hq0A0: q0 ∈ A0.
An exact proof term for the current goal is (andEL (q0 ∈ A0) (q0 ∈ N) Hq0AN).
We prove the intermediate claim Hq0N: q0 ∈ N.
An exact proof term for the current goal is (andER (q0 ∈ A0) (q0 ∈ N) Hq0AN).
We prove the intermediate claim Hq0X: q0 ∈ X.
An exact proof term for the current goal is (open_ballE1 X d p r q0 Hq0N).
We prove the intermediate claim Hq0Bp: Rlt (apply_fun d (p,q0)) r.
An exact proof term for the current goal is (open_ballE2 X d p r q0 Hq0N).
We prove the intermediate claim Hq0Px: Rlt (apply_fun d (q0,p)) r.
rewrite the current goal using (metric_on_symmetric X d p q0 Hm HpX Hq0X) (from right to left).
An exact proof term for the current goal is Hq0Bp.
We prove the intermediate claim Hq0Bx0: q0 ∈ open_ball X d x0 r.
rewrite the current goal using HA0eq (from right to left).
An exact proof term for the current goal is Hq0A0.
We prove the intermediate claim Hq0x0: Rlt (apply_fun d (x0,q0)) r.
An exact proof term for the current goal is (open_ballE2 X d x0 r q0 Hq0Bx0).
We prove the intermediate claim Hx0X: x0 ∈ X.
An exact proof term for the current goal is ((andEL (S ⊆ X) (∀a b : set, a ∈ S → b ∈ S → ¬ (a = b) → ¬ (Rlt (apply_fun d (a,b)) (eps_ n))) Hsep) x0 Hx0S).
We prove the intermediate claim Htri: Rle (apply_fun d (x0,p)) (add_SNo (apply_fun d (x0,q0)) (apply_fun d (q0,p))).
An exact proof term for the current goal is (metric_triangle_Rle X d x0 q0 p Hm Hx0X Hq0X HpX).
We prove the intermediate claim HsumLt: Rlt (add_SNo (apply_fun d (x0,q0)) (apply_fun d (q0,p))) (add_SNo r r).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun d (x0,q0)) r (apply_fun d (q0,p)) r Hq0x0 Hq0Px).
We prove the intermediate claim HdistLt: Rlt (apply_fun d (x0,p)) (add_SNo r r).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (x0,p)) (add_SNo (apply_fun d (x0,q0)) (apply_fun d (q0,p))) (add_SNo r r) Htri HsumLt).
We prove the intermediate claim Hnat1: nat_p (ordsucc n).
An exact proof term for the current goal is (omega_nat_p (ordsucc n) Hsucc1).
We prove the intermediate claim HrrEps: add_SNo r r = eps_ (ordsucc n).
rewrite the current goal using (eps_ordsucc_half_add (ordsucc n) Hnat1) (from right to left).
Use reflexivity.
We prove the intermediate claim HpBig0: p ∈ open_ball X d x0 (eps_ (ordsucc n)).
rewrite the current goal using HrrEps (from right to left).
An exact proof term for the current goal is (open_ballI X d x0 (add_SNo r r) p HpX HdistLt).
We prove the intermediate claim Huniq: ∀A : set, A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S} → A ∩ N ≠ Empty → A = A0.
Let A be given.
Assume HAinF: A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
Assume HAmeet: A ∩ N ≠ Empty.
Apply (ReplE S (λx : set ⇒ open_ball X d x r) A HAinF) to the current goal.
Let x1 be given.
Assume Hx1pack.
We prove the intermediate claim Hx1S: x1 ∈ S.
An exact proof term for the current goal is (andEL (x1 ∈ S) (A = open_ball X d x1 r) Hx1pack).
We prove the intermediate claim HAeq: A = open_ball X d x1 r.
An exact proof term for the current goal is (andER (x1 ∈ S) (A = open_ball X d x1 r) Hx1pack).
We prove the intermediate claim Hexq: ∃q : set, q ∈ (A ∩ N).
An exact proof term for the current goal is (nonempty_has_element (A ∩ N) HAmeet).
Apply Hexq to the current goal.
Let q be given.
Assume Hqin.
We prove the intermediate claim HqAN: q ∈ A ∧ q ∈ N.
An exact proof term for the current goal is (binintersectE A N q Hqin).
We prove the intermediate claim HqA: q ∈ A.
An exact proof term for the current goal is (andEL (q ∈ A) (q ∈ N) HqAN).
We prove the intermediate claim HqN: q ∈ N.
An exact proof term for the current goal is (andER (q ∈ A) (q ∈ N) HqAN).
We prove the intermediate claim HqX: q ∈ X.
An exact proof term for the current goal is (open_ballE1 X d p r q HqN).
We prove the intermediate claim HqBp: Rlt (apply_fun d (p,q)) r.
An exact proof term for the current goal is (open_ballE2 X d p r q HqN).
We prove the intermediate claim HqPp: Rlt (apply_fun d (q,p)) r.
rewrite the current goal using (metric_on_symmetric X d p q Hm HpX HqX) (from right to left).
An exact proof term for the current goal is HqBp.
We prove the intermediate claim HqBx1: q ∈ open_ball X d x1 r.
rewrite the current goal using HAeq (from right to left).
An exact proof term for the current goal is HqA.
We prove the intermediate claim HqX1: x1 ∈ X.
An exact proof term for the current goal is ((andEL (S ⊆ X) (∀a b : set, a ∈ S → b ∈ S → ¬ (a = b) → ¬ (Rlt (apply_fun d (a,b)) (eps_ n))) Hsep) x1 Hx1S).
We prove the intermediate claim Hqx1: Rlt (apply_fun d (x1,q)) r.
An exact proof term for the current goal is (open_ballE2 X d x1 r q HqBx1).
We prove the intermediate claim Htri1: Rle (apply_fun d (x1,p)) (add_SNo (apply_fun d (x1,q)) (apply_fun d (q,p))).
An exact proof term for the current goal is (metric_triangle_Rle X d x1 q p Hm HqX1 HqX HpX).
We prove the intermediate claim HsumLt1: Rlt (add_SNo (apply_fun d (x1,q)) (apply_fun d (q,p))) (add_SNo r r).
An exact proof term for the current goal is (Rlt_add_SNo (apply_fun d (x1,q)) r (apply_fun d (q,p)) r Hqx1 HqPp).
We prove the intermediate claim HdistLt1: Rlt (apply_fun d (x1,p)) (add_SNo r r).
An exact proof term for the current goal is (Rle_Rlt_tra (apply_fun d (x1,p)) (add_SNo (apply_fun d (x1,q)) (apply_fun d (q,p))) (add_SNo r r) Htri1 HsumLt1).
We prove the intermediate claim HpBig1: p ∈ open_ball X d x1 (eps_ (ordsucc n)).
rewrite the current goal using HrrEps (from right to left).
An exact proof term for the current goal is (open_ballI X d x1 (add_SNo r r) p HpX HdistLt1).
We prove the intermediate claim Hx1eqx0: x1 = x0.
An exact proof term for the current goal is (eps_separated_imp_eps_succ_ball_point_unique X d S n p x1 x0 Hm HnO Hsep HpX Hx1S Hx0S HpBig1 HpBig0).
rewrite the current goal using HA0eq (from left to right).
rewrite the current goal using HAeq (from left to right).
rewrite the current goal using Hx1eqx0 (from left to right).
Use reflexivity.
We use {A0} 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 (Sing_finite A0).
Let y be given.
Assume Hy: y ∈ {A0}.
We will prove y ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
rewrite the current goal using (SingE A0 y Hy) (from left to right).
An exact proof term for the current goal is HA0inF.
Let A be given.
Assume HAinF: A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
Assume HAmeet: A ∩ N ≠ Empty.
We prove the intermediate claim HAeqA0: A = A0.
An exact proof term for the current goal is (Huniq A HAinF HAmeet).
rewrite the current goal using HAeqA0 (from left to right).
An exact proof term for the current goal is (SingI A0).
Assume HnoA.
We use Empty 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 finite_Empty.
An exact proof term for the current goal is (Subq_Empty {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}).
Let A be given.
Assume HAinF: A ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S}.
Assume HAmeet: A ∩ N ≠ Empty.
We prove the intermediate claim Hex: ∃A0 : set, A0 ∈ {open_ball X d x (eps_ (ordsucc (ordsucc n)))|x ∈ S} ∧ A0 ∩ N ≠ Empty.
We use A to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HAinF.
An exact proof term for the current goal is HAmeet.
We prove the intermediate claim Hcontra: False.
An exact proof term for the current goal is (HnoA Hex).
An exact proof term for the current goal is (FalseE Hcontra (A ∈ Empty)).
∎