no goals
α✝ : Type ?u.190164
β : Type ?u.190167
γ : Type ?u.190170
δ : Type ?u.190173
inst✝ : TopologicalSpace α✝
α : Type u_1
s : Set α
t : Set ↑s
⊢ 𝓟 t = comap Subtype.val (𝓟 (Subtype.val '' t))
rw [comap_principal, preimage_image_eq _ Subtype.coe_injective]