Theorem: RegularOpens.coe_inf (LeanCourse/Lectures/Lecture11.lean)

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V
Tactic:
have : U ⊓ V = (U.cl ⊓ V.cl).int := rfl
State after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊓ V = Closeds.int (cl U ⊓ cl V)
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
this : U ⊓ V = Closeds.int (cl U ⊓ cl V)
⊢ ↑(U ⊓ V) = ↑U ∩ ↑V
Tactic:
simp [this]
State after:
no goals