no goals
α : Type ?u.52656
β : Type ?u.52659
G₀ : Type u_1
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ map (fun x => a * x) (𝓝 1) = 𝓝 a
rw [map_mul_left_nhds₀ ha, mul_one]