We will prove metric_topology EuclidPlane EuclidPlane_metric = generated_topology EuclidPlane circular_regions.

rewrite the current goal using (metric_topology_generated_by_balls EuclidPlane EuclidPlane_metric EuclidPlane_metric_is_metric_on) (from right to left).

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

Use reflexivity.

∎