Let X, d and U be given.

Assume Hm: metric_on X d.

Set Tx to be the term metric_topology X d.

We prove the intermediate claim HTx: topology_on X Tx.

An exact proof term for the current goal is (metric_topology_is_topology X d Hm).

We prove the intermediate claim HexV: ∃V : set, open_cover X Tx V ∧ locally_finite_family X Tx V ∧ refine_of V U.

An exact proof term for the current goal is (metric_open_cover_has_locally_finite_refinement X d U Hm Hcov).

Apply HexV to the current goal.

Let V be given.

Assume HVpack.

We use V to witness the existential quantifier.

We prove the intermediate claim HVleft: open_cover X Tx V ∧ locally_finite_family X Tx V.

An exact proof term for the current goal is (andEL (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V U) HVpack).

We prove the intermediate claim HVcov: open_cover X Tx V.

An exact proof term for the current goal is (andEL (open_cover X Tx V) (locally_finite_family X Tx V) HVleft).

We prove the intermediate claim HVlf: locally_finite_family X Tx V.

An exact proof term for the current goal is (andER (open_cover X Tx V) (locally_finite_family X Tx V) HVleft).

We prove the intermediate claim HVref: refine_of V U.

An exact proof term for the current goal is (andER (open_cover X Tx V ∧ locally_finite_family X Tx V) (refine_of V U) HVpack).

We prove the intermediate claim HVsubPow: V ⊆ 𝒫 X.

An exact proof term for the current goal is (open_cover_family_sub X Tx V HTx HVcov).

We prove the intermediate claim HVsigma: sigma_locally_finite_family X Tx V.

An exact proof term for the current goal is (locally_finite_family_imp_sigma_locally_finite_family X Tx V HTx HVsubPow HVlf).

Apply andI to the current goal.

An exact proof term for the current goal is HVcov.

An exact proof term for the current goal is HVsigma.

An exact proof term for the current goal is HVref.

∎