no goals
α : Type u_1
β : Type u_2
γ : Type ?u.1466
δ : Type ?u.1469
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : Inducing f
s : Set α
⊢ 𝓝ˢ s = comap f (𝓝ˢ (f '' s))
simp only [nhdsSet, sSup_image, comap_iSup, hf.nhds_eq_comap, iSup_image]