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

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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U V : RegularOpens X
this : ⊤ = Closeds.int ⊤
⊢ ↑⊤ = univ
Tactic:
simp [this]
State after:
no goals