Theorem: inv_tendsto_atInf' (Ray/Misc/AtInf.lean)

State before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x⁻¹) atInf (𝓝 0)
Tactic:
simp only [tendsto_atInf_iff_tendsto_nhds_zero, inv_inv]
State after:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) (𝓝[≠] 0) (𝓝 0)

State before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) (𝓝[≠] 0) (𝓝 0)
Tactic:
exact Filter.tendsto_id.mono_left nhdsWithin_le_nhds
State after:
no goals