Let X, d, Y, S and n be given.
Assume Hm: metric_on X d.
Assume HnO: n ∈ ω.
Assume Hmax: maximal_eps_separated_set_on X d Y S n.
Apply (and4E (Y ⊆ X) (S ⊆ Y) (∀x y : set, x ∈ S → y ∈ S → ¬ (x = y) → ¬ (Rlt (apply_fun d (x,y)) (eps_ n))) (∀x : set, x ∈ Y → (∀y : set, y ∈ S → ¬ (Rlt (apply_fun d (x,y)) (eps_ n))) → x ∈ S) Hmax) to the current goal.
Assume HYsubX HSsubY HsepProp HmaxProp.
We will prove Y ⊆ (⋃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 HxY: x ∈ Y.
We will prove x ∈ U.
We prove the intermediate claim HxX: x ∈ X.
An exact proof term for the current goal is (HYsubX x HxY).
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 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 HyY: y ∈ Y.
An exact proof term for the current goal is (HSsubY y HyS).
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (HYsubX y HyY).
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 (HmaxProp x HxY 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).
∎