no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
⊢ s \ frontier s = interior s
rw [frontier, diff_diff_right, diff_eq_empty.2 subset_closure,
  inter_eq_self_of_subset_right interior_subset, empty_union]