Let X and Tx be given.

Assume Hmet: metrizable X Tx.

We will prove paracompact_space X Tx.

Apply Hmet to the current goal.

Let d be given.

Assume Hdpair: metric_on X d ∧ metric_topology X d = Tx.

We prove the intermediate claim Hm: metric_on X d.

An exact proof term for the current goal is (andEL (metric_on X d) (metric_topology X d = Tx) Hdpair).

We prove the intermediate claim Heq: metric_topology X d = Tx.

An exact proof term for the current goal is (andER (metric_on X d) (metric_topology X d = Tx) Hdpair).

rewrite the current goal using Heq (from right to left).

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

∎