We will prove metric_topology EuclidPlane EuclidPlane_metric = generated_topology EuclidPlane rectangular_regions.

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

An exact proof term for the current goal is (circular_rectangular_same_topology_plane).

∎