Let X, Tx and A be given.
Assume Hmet: metrizable X Tx.
Assume HA: A ⊆ X.
We will prove ∃dA : set, metric_on A dA ∧ metric_topology A dA = subspace_topology X Tx A.
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 Hd: 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).
We use (metric_restrict X d A) to witness the existential quantifier.
Apply andI to the current goal.
An exact proof term for the current goal is (metric_restrict_is_metric_on X d A Hd HA).
We prove the intermediate claim Hsubeq: metric_topology A (metric_restrict X d A) = subspace_topology X (metric_topology X d) A.
An exact proof term for the current goal is (metric_topology_restrict_eq_subspace_topology X d A Hd HA).
rewrite the current goal using Hsubeq (from left to right).
rewrite the current goal using Heq (from left to right).
Use reflexivity.
∎