Let X and d be given.

Assume Hm: metric_on X d.

We will prove paracompact_space X (metric_topology X d).

We will prove topology_on X (metric_topology X d) ∧ ∀U : set, open_cover X (metric_topology X d) U → ∃V : set, open_cover X (metric_topology X d) V ∧ locally_finite_family X (metric_topology X d) V ∧ refine_of V U.

Apply andI to the current goal.

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

Let U be given.

Assume Hcov: open_cover X (metric_topology X d) U.

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

∎