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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V✝ U V : RegularOpens X
⊢ ↑(U ⊔ V) = interior (closure (↑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) = interior (closure (↑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) = interior (closure (↑U ∪ ↑V))
Tactic:
simp [this]
State after:
no goals