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

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

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