Let X, d, c, x and r be given.
Assume Hm: metric_on X d.
Assume Hc: c ∈ X.
Assume HxX: x ∈ X.
Assume HrR: r ∈ R.
Assume Hrpos: Rlt 0 r.
Assume Hxin: x ∈ open_ball X d c r.
We prove the intermediate claim Hexs: ∃s : set, s ∈ R ∧ Rlt 0 s ∧ open_ball X d x s ⊆ open_ball X d c r.
An exact proof term for the current goal is (open_ball_refine_center X d c x r Hm Hc HxX HrR Hrpos Hxin).
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 r) HsPack).
We prove the intermediate claim HsSub: open_ball X d x s ⊆ open_ball X d c r.
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 r) 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 HexN: ∃N ∈ ω, eps_ N < s.
An exact proof term for the current goal is (exists_eps_lt_pos 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 HepsLt: eps_ N < s.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < s) HNpair).
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 HNomega)).
We prove the intermediate claim HepsRlt: Rlt (eps_ N) s.
An exact proof term for the current goal is (RltI (eps_ N) s HepsR HsR HepsLt).
We prove the intermediate claim Hsub1: open_ball X d x (eps_ N) ⊆ open_ball X d x s.
Let y be given.
Assume Hy: y ∈ open_ball X d x (eps_ N).
We will prove y ∈ open_ball X d x s.
We prove the intermediate claim HyX: y ∈ X.
An exact proof term for the current goal is (open_ballE1 X d x (eps_ N) y Hy).
We prove the intermediate claim Hdlt: Rlt (apply_fun d (x,y)) (eps_ N).
An exact proof term for the current goal is (open_ballE2 X d x (eps_ N) y Hy).
We prove the intermediate claim Hdlt2: Rlt (apply_fun d (x,y)) s.
An exact proof term for the current goal is (Rlt_tra (apply_fun d (x,y)) (eps_ N) s Hdlt HepsRlt).
An exact proof term for the current goal is (open_ballI X d x s y HyX Hdlt2).
We prove the intermediate claim Hsub2: open_ball X d x (eps_ N) ⊆ open_ball X d c r.
An exact proof term for the current goal is (Subq_tra (open_ball X d x (eps_ N)) (open_ball X d x s) (open_ball X d c r) Hsub1 HsSub).
We use N to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HNomega.
An exact proof term for the current goal is Hsub2.
∎