We will prove metric_topology EuclidPlane EuclidPlane_metric = R2_standard_topology.

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

An exact proof term for the current goal is generated_topology_rectangular_regions_eq_R2_standard_topology.

∎