rw [nhdsWithin_eq_map_subtype_coe (hst a.prop), Filter.frequently_map,
  clusterPt_principal_iff_frequently, inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap,
  inducing_subtype_val.nhds_eq_comap, Filter.frequently_comap, Subtype.coe_mk]
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ ClusterPt a (𝓟 J) ↔ ∃ᶠ (x : α) in nhdsWithin (↑a) t, ∃ (h : x ∈ s), { val := x, property := h } ∈ J
α✝ : Type ?u.2106
α : Type u_1
inst✝ : TopologicalSpace α
s t : Set α
hst : s ⊆ t
J : Set ↑s
a : ↑s
⊢ (∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ a ∈ J) ↔
    ∃ᶠ (b : α) in nhds ↑a, ∃ a, ↑a = b ∧ ∃ (h : ↑a ∈ s), { val := ↑a, property := h } ∈ J