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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))
Tactic:
have : sSup U = (sSup (cl '' U)).int := rfl
State after:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sSup U = Closeds.int (sSup (cl '' U))
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V : RegularOpens X
U : Set (RegularOpens X)
this : sSup U = Closeds.int (sSup (cl '' U))
⊢ ↑(sSup U) = interior (closure (⋃₀ ((fun u => closure ↑u) '' U)))
Tactic:
simp [this]
State after:
no goals