no goals
α : Type ?u.57877
β : Type ?u.57880
G₀ : Type u_1
inst✝² : TopologicalSpace G₀
inst✝¹ : GroupWithZero G₀
inst✝ : ContinuousMul G₀
a : G₀
ha : a ≠ 0
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.symm (Homeomorph.mulRight₀ a ha))) 1) = 𝓝 a
simp