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

State before:
X : Type u_1
inst✝ : TopologicalSpace X
U✝ V U : RegularOpens X
⊢ ↑Uᶜ = interior (↑U)ᶜ
Tactic:
sorry
State after:
no goals