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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))
Tactic:
have : sSup C = Closeds.closure (sSup ((↑) '' C)) := rfl
State after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(sSup C) = closure (⋃₀ (SetLike.coe '' C))
Tactic:
simp [this]
State after:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(Closeds.closure (⋃ x ∈ C, ↑x)) = closure (⋃ x ∈ C, ↑x)

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
C : Set (Closeds X)
this : sSup C = Closeds.closure (sSup (SetLike.coe '' C))
⊢ ↑(Closeds.closure (⋃ x ∈ C, ↑x)) = closure (⋃ x ∈ C, ↑x)
Tactic:
rfl
State after:
no goals