no goals
α : Type u_1
β : Type ?u.400653
γ : Type ?u.400656
δ : Type ?u.400659
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
s t : Set α
ht : IsOpen t
⊢ frontier (s ∩ t) ∩ t = frontier s ∩ t
simp only [← Subtype.preimage_coe_eq_preimage_coe_iff,
  ht.isOpenMap_subtype_val.preimage_frontier_eq_frontier_preimage continuous_subtype_val,
  Subtype.preimage_coe_inter_self]