[Merged by Bors] - feat(Analysis): tendsto_zpow_nhdsNE_zero_cobounded

Mathlib/Analysis/Normed/Field/Lemmas.lean

@@ -80,17 +80,22 @@ lemma inv_cobounded₀ : (cobounded α)⁻¹ = 𝓝[≠] 0 := by
   simp only [comap_comap, Function.comp_def, norm_inv]
 
 @[simp]
-lemma inv_nhdsWithin_ne_zero : (𝓝[≠] (0 : α))⁻¹ = cobounded α := by
+lemma inv_nhdsNE_zero : (𝓝[≠] (0 : α))⁻¹ = cobounded α := by
   rw [← inv_cobounded₀, inv_inv]
 
+@[deprecated (since := "2025-11-26")] alias inv_nhdsWithin_ne_zero := inv_nhdsNE_zero
+
 lemma tendsto_inv₀_cobounded' : Tendsto Inv.inv (cobounded α) (𝓝[≠] 0) :=
   inv_cobounded₀.le
 
 theorem tendsto_inv₀_cobounded : Tendsto Inv.inv (cobounded α) (𝓝 0) :=
   tendsto_inv₀_cobounded'.mono_right inf_le_left
 
-lemma tendsto_inv₀_nhdsWithin_ne_zero : Tendsto Inv.inv (𝓝[≠] 0) (cobounded α) :=
-  inv_nhdsWithin_ne_zero.le
+lemma tendsto_inv₀_nhdsNE_zero : Tendsto Inv.inv (𝓝[≠] 0) (cobounded α) :=
+  inv_nhdsNE_zero.le
+
+@[deprecated (since := "2025-11-26")]
+alias tendsto_inv₀_nhdsWithin_ne_zero := tendsto_inv₀_nhdsNE_zero
 
 end Filter
 
@@ -121,16 +126,18 @@ instance (priority := 100) NormedDivisionRing.to_isTopologicalDivisionRing :
     IsTopologicalDivisionRing α where
 
 lemma NormedField.tendsto_norm_inv_nhdsNE_zero_atTop : Tendsto (fun x : α ↦ ‖x⁻¹‖) (𝓝[≠] 0) atTop :=
-  (tendsto_inv_nhdsGT_zero.comp tendsto_norm_nhdsNE_zero).congr fun x ↦ (norm_inv x).symm
+  tendsto_norm_cobounded_atTop.comp tendsto_inv₀_nhdsNE_zero
 
-lemma NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) :
-    Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop := by
+lemma NormedField.tendsto_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) :
+    Tendsto (· ^ m) (𝓝[≠] 0) (Bornology.cobounded α) := by
   obtain ⟨m, rfl⟩ := neg_surjective m
-  rw [neg_lt_zero] at hm
-  lift m to ℕ using hm.le
-  rw [Int.natCast_pos] at hm
-  simp only [norm_pow, zpow_neg, zpow_natCast, ← inv_pow]
-  exact (tendsto_pow_atTop hm.ne').comp NormedField.tendsto_norm_inv_nhdsNE_zero_atTop
+  lift m to ℕ using by cutsat
+  simpa [Function.comp_def] using (SeminormedRing.tendsto_pow_cobounded_cobounded
+    (by cutsat)).comp tendsto_inv₀_nhdsNE_zero
+
+lemma NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop {m : ℤ} (hm : m < 0) :
+    Tendsto (fun x : α ↦ ‖x ^ m‖) (𝓝[≠] 0) atTop :=
+  tendsto_norm_cobounded_atTop.comp (tendsto_zpow_nhdsNE_zero_atTop hm)
 
 end NormedDivisionRing
 

Mathlib/Analysis/Normed/Ring/Lemmas.lean

@@ -75,6 +75,12 @@ lemma RingHomIsometric.inv {𝕜₁ 𝕜₂ : Type*} [SeminormedRing 𝕜₁] [S
     RingHomIsometric σ' :=
   ⟨fun {x} ↦ by rw [← RingHomIsometric.norm_map (σ := σ), RingHomInvPair.comp_apply_eq₂]⟩
 
+lemma SeminormedRing.tendsto_pow_cobounded_cobounded
+    [NormOneClass α] [NormMulClass α] {m : ℕ} (hm : m ≠ 0) :
+    Tendsto (· ^ m) (Bornology.cobounded α) (Bornology.cobounded α) := by
+  simpa [← tendsto_norm_atTop_iff_cobounded] using
+    (tendsto_pow_atTop hm).comp (tendsto_norm_cobounded_atTop (E := α))
+
 end SeminormedRing
 
 section NonUnitalNormedRing