Let X, d and U be given.
Assume Hm: metric_on X d.
Assume Hcov: open_cover X (metric_topology X d) U.
We will prove ∃V : set, open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V ∧ refine_of V U.
We prove the intermediate claim HexB: ∃B : set, open_cover X (metric_topology X d) B ∧ (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) ∧ refine_of B U.
An exact proof term for the current goal is (metric_open_cover_refine_by_balls X d U Hm Hcov).
Apply HexB to the current goal.
Let B be given.
Assume HBpack.
We prove the intermediate claim HBleft: (open_cover X (metric_topology X d) B ∧ (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r)).
An exact proof term for the current goal is (andEL (open_cover X (metric_topology X d) B ∧ (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r)) (refine_of B U) HBpack).
We prove the intermediate claim HBcov: open_cover X (metric_topology X d) B.
An exact proof term for the current goal is (andEL (open_cover X (metric_topology X d) B) (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) HBleft).
We prove the intermediate claim HBballs: ∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r.
An exact proof term for the current goal is (andER (open_cover X (metric_topology X d) B) (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r) HBleft).
We prove the intermediate claim HBref: refine_of B U.
An exact proof term for the current goal is (andER (open_cover X (metric_topology X d) B ∧ (∀b : set, b ∈ B → ∃x ∈ X, ∃r ∈ R, Rlt 0 r ∧ b = open_ball X d x r)) (refine_of B U) HBpack).
We prove the intermediate claim HexV: ∃V : set, open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V ∧ refine_of V B.
An exact proof term for the current goal is (metric_ball_open_cover_has_locally_finite_refinement X d B Hm HBcov HBballs).
Apply HexV to the current goal.
Let V be given.
Assume HVpack.
We use V to witness the existential quantifier.
Apply andI to the current goal.
We prove the intermediate claim HVleft: (open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V).
An exact proof term for the current goal is (andEL (open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V) (refine_of V B) HVpack).
Apply andI to the current goal.
An exact proof term for the current goal is (andEL (open_cover X (metric_topology X d) V) (locally_finite_family X (metric_topology X d) V) HVleft).
An exact proof term for the current goal is (andER (open_cover X (metric_topology X d) V) (locally_finite_family X (metric_topology X d) V) HVleft).
An exact proof term for the current goal is (refine_trans U B V (andER (open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V) (refine_of V B) HVpack) HBref).
∎