Let X and Tx be given.
Apply iffI to the current goal.
Assume Hmet: metrizable X Tx.
We will prove regular_space X Tx ∧ sigma_locally_finite_basis 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).
Apply andI to the current goal.
rewrite the current goal using Heq (from right to left).
We prove the intermediate claim Hcr: completely_regular_space X (metric_topology X d).
An exact proof term for the current goal is (metric_spaces_completely_regular X d Hm).
An exact proof term for the current goal is (completely_regular_space_implies_regular X (metric_topology X d) Hcr).
rewrite the current goal using Heq (from right to left).
An exact proof term for the current goal is (metric_space_sigma_locally_finite_basis X d Hm).
Assume H: regular_space X Tx ∧ sigma_locally_finite_basis X Tx.
We will prove metrizable X Tx.
An exact proof term for the current goal is (Nagata_Smirnov_metrization X Tx (andEL (regular_space X Tx) (sigma_locally_finite_basis X Tx) H) (andER (regular_space X Tx) (sigma_locally_finite_basis X Tx) H)).
∎