Let X, d, U and x be given.
Assume Hm: metric_on X d.
Assume Hcov: open_cover X (metric_topology X d) U.
Assume HxX: x ∈ X.
We will prove ∃u : set, u ∈ U ∧ ∃N : set, N ∈ ω ∧ open_ball X d x (eps_ N) ⊆ u.
We prove the intermediate claim Hexur: ∃u : set, u ∈ U ∧ ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u).
An exact proof term for the current goal is (metric_open_cover_point_ball_submember X d U x Hm Hcov HxX).
Apply Hexur to the current goal.
Let u be given.
Assume Hupack.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u)) Hupack).
We prove the intermediate claim Hexr: ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u).
An exact proof term for the current goal is (andER (u ∈ U) (∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u)) Hupack).
Apply Hexr to the current goal.
Let r be given.
Assume Hrpack.
We prove the intermediate claim HrR: r ∈ R.
An exact proof term for the current goal is (andEL (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrrest: Rlt 0 r ∧ open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (r ∈ R) (Rlt 0 r ∧ open_ball X d x r ⊆ u) Hrpack).
We prove the intermediate claim Hrpos: Rlt 0 r.
An exact proof term for the current goal is (andEL (Rlt 0 r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim Hsubu: open_ball X d x r ⊆ u.
An exact proof term for the current goal is (andER (Rlt 0 r) (open_ball X d x r ⊆ u) Hrrest).
We prove the intermediate claim HexN: ∃N ∈ ω, eps_ N < r.
An exact proof term for the current goal is (exists_eps_lt_pos r HrR Hrpos).
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 < r) HNpair).
We prove the intermediate claim HepsLt: eps_ N < r.
An exact proof term for the current goal is (andER (N ∈ ω) (eps_ N < r) 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) r.
An exact proof term for the current goal is (RltI (eps_ N) r HepsR HrR HepsLt).
We prove the intermediate claim Hsub1: open_ball X d x (eps_ N) ⊆ open_ball X d x r.
Let y be given.
Assume Hy: y ∈ open_ball X d x (eps_ N).
We will prove y ∈ open_ball X d x r.
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)) r.
An exact proof term for the current goal is (Rlt_tra (apply_fun d (x,y)) (eps_ N) r Hdlt HepsRlt).
An exact proof term for the current goal is (open_ballI X d x r y HyX Hdlt2).
We prove the intermediate claim Hsub2: open_ball X d x (eps_ N) ⊆ u.
An exact proof term for the current goal is (Subq_tra (open_ball X d x (eps_ N)) (open_ball X d x r) u Hsub1 Hsubu).
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
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.
∎