no goals
α : Type u_1
β : Type ?u.376392
γ : Type ?u.376395
ι : Type ?u.376398
inst✝ : NontriviallyNormedField α
⊢ NeBot (𝓝[{x | IsUnit x}] 0)
simpa only [isUnit_iff_ne_zero] using punctured_nhds_neBot (0 : α)