T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (pretopology T) = grothendieckTopology T
rw [← pretopology_ofGrothendieck]
no goals
T : Type u
inst✝ : TopologicalSpace T
⊢ Pretopology.toGrothendieck (Opens T) (Pretopology.ofGrothendieck (Opens T) (grothendieckTopology T)) =
    grothendieckTopology T
apply (Pretopology.gi (Opens T)).l_u_eq