no goals
α : Type u
β : Type v
γ : Type ?u.44785
f✝ : α → β
ι : Sort ?u.44792
tα : TopologicalSpace α
tβ : TopologicalSpace β
f : β → α
h : ∀ (b : β), 𝓝 b = comap f (𝓝 (f b))
x : β
⊢ 𝓝 x = 𝓝 x
rw [h, nhds_induced]