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 ∧ ∃r : set, r ∈ R ∧ (Rlt 0 r ∧ open_ball X d x r ⊆ u).
We prove the intermediate claim Hcovers: covers X U.
An exact proof term for the current goal is (open_cover_implies_covers X (metric_topology X d) U Hcov).
We prove the intermediate claim Hexu: ∃u : set, u ∈ U ∧ x ∈ u.
An exact proof term for the current goal is (Hcovers x HxX).
Apply Hexu to the current goal.
Let u be given.
Assume Hupair: u ∈ U ∧ x ∈ u.
We prove the intermediate claim HuU: u ∈ U.
An exact proof term for the current goal is (andEL (u ∈ U) (x ∈ u) Hupair).
We prove the intermediate claim Hxu: x ∈ u.
An exact proof term for the current goal is (andER (u ∈ U) (x ∈ u) Hupair).
We prove the intermediate claim HuTop: u ∈ metric_topology X d.
An exact proof term for the current goal is (open_cover_members_open X (metric_topology X d) U u Hcov HuU).
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 (metric_topology_neighborhood_contains_ball X d x u Hm HxX HuTop Hxu).
We use u to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is HuU.
An exact proof term for the current goal is Hexr.
∎