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

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

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