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

State before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x⁻¹) (𝓝[≠] 0) atInf
Tactic:
rw [←tendsto_atInf_iff_tendsto_nhds_zero (f := fun x : 𝕜 ↦ x)]
State after:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) atInf atInf

State before:
𝕜 : Type
inst✝ : NontriviallyNormedField 𝕜
⊢ Tendsto (fun x => x) atInf atInf
Tactic:
exact Filter.tendsto_id
State after:
no goals