Let X, d, S and n be given.
Assume Hm: metric_on X d.
Assume HnO: n ∈ ω.
Assume Hmax: maximal_eps_separated_set X d S n.
We will prove X ⊆ (⋃c ∈ Sopen_ball X d c (eps_ n)).
Set U to be the term (⋃c ∈ Sopen_ball X d c (eps_ n)).
Let x be given.
Assume HxX: x ∈ X.
We will prove x ∈ U.
Apply (xm (x ∈ U)) to the current goal.
Assume HxU: x ∈ U.
An exact proof term for the current goal is HxU.
Assume HxNotU: ¬ (x ∈ U).
We prove the intermediate claim Hsep: eps_separated_set X d S n.
An exact proof term for the current goal is (andEL (eps_separated_set X d S n) (∀x0 : set, x0 ∈ X → (∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x0,y)) (eps_ n))) → x0 ∈ S) Hmax).
We prove the intermediate claim HSsubX: S ⊆ X.
An exact proof term for the current goal is (andEL (S ⊆ X) (∀x0 y0 : set, x0 ∈ S → y0 ∈ S → ¬ (x0 = y0) → ¬ (Rlt (apply_fun d (x0,y0)) (eps_ n))) Hsep).
We prove the intermediate claim Hfar: ∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x,y)) (eps_ n)).
Let y be given.
Assume HyS: y ∈ S.
Assume Hlt: Rlt (apply_fun d (x,y)) (eps_ n).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HSsubX y HyS).
We prove the intermediate claim Hsym: Rlt (apply_fun d (y,x)) (eps_ n).
rewrite the current goal using (metric_on_symmetric X d x y Hm HxX HyX) (from right to left).
An exact proof term for the current goal is Hlt.
We prove the intermediate claim HxBall: x ∈ open_ball X d y (eps_ n).
An exact proof term for the current goal is (open_ballI X d y (eps_ n) x HxX Hsym).
We prove the intermediate claim HxU2: x ∈ U.
An exact proof term for the current goal is (famunionI S (λc : set ⇒ open_ball X d c (eps_ n)) y x HyS HxBall).
An exact proof term for the current goal is (HxNotU HxU2).
We prove the intermediate claim HxS: x ∈ S.
An exact proof term for the current goal is ((andER (eps_separated_set X d S n) (∀x0 : set, x0 ∈ X → (∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x0,y)) (eps_ n))) → x0 ∈ S) Hmax) x HxX Hfar).
We prove the intermediate claim HepsR: eps_ n ∈ R.
An exact proof term for the current goal is (SNoS_omega_real (eps_ n) (SNo_eps_SNoS_omega n HnO)).
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 (SNo_eps_pos n HnO)).
We prove the intermediate claim HxBall: x ∈ open_ball X d x (eps_ n).
An exact proof term for the current goal is (center_in_open_ball X d x (eps_ n) Hm HxX HepsPos).
An exact proof term for the current goal is (famunionI S (λc : set ⇒ open_ball X d c (eps_ n)) x x HxS HxBall).
∎