this : (exp ⁻¹' {0})ᶜ = Set.univ
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
have : (exp ⁻¹' {0})ᶜ = Set.univ := eq_univ_of_forall exp_ne_zero
no goals
this : (exp ⁻¹' {0})ᶜ = Set.univ
⊢ comap exp (𝓝[{0}ᶜ] 0) = comap re atBot
simp [nhdsWithin, comap_exp_nhds_zero, this]