chore(Analysis/SpecificLimits/Basic): generalize lemmas (#28475)

Author: astrainfinita

Counterexamples/DiscreteTopologyNonDiscreteUniformity.lean

@@ -3,12 +3,7 @@ Copyright (c) 2024 Filippo A. E. Nuccio. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Filippo A. E. Nuccio
 -/
-
 import Mathlib.Analysis.SpecificLimits.Basic
-import Mathlib.Order.Interval.Set.Basic
-import Mathlib.Topology.MetricSpace.Pseudo.Defs
-import Mathlib.Topology.MetricSpace.Cauchy
-import Mathlib.Topology.UniformSpace.Cauchy
 
 /-!
 # Discrete uniformities and discrete topology
@@ -83,11 +78,10 @@ open Set Function Filter Metric
 
 /- We remove the "usual" instances of (discrete) topological space and of (discrete) uniform space
 from `ℕ`. -/
-attribute [-instance] instTopologicalSpaceNat instUniformSpaceNat
+attribute [-instance] instTopologicalSpaceNat instUniformSpaceNat Nat.instDist
 
 section Metric
 
-
 noncomputable local instance : PseudoMetricSpace ℕ where
   dist := fun n m ↦ |2 ^ (- n : ℤ) - 2 ^ (- m : ℤ)|
   dist_self := by simp only [zpow_neg, zpow_natCast, sub_self, abs_zero, implies_true]

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -117,7 +117,7 @@ theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {a : A} (ha : IsSelfAdjoint a) :
   refine tendsto_nhds_unique ?_ hconst
   convert
     (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
-      (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1
+      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1
   refine funext fun n => ?_
   rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]
   simp

Mathlib/Analysis/Normed/Algebra/Exponential.lean

@@ -8,7 +8,6 @@ import Mathlib.Analysis.Analytic.ChangeOrigin
 import Mathlib.Analysis.Complex.Basic
 import Mathlib.Data.Nat.Choose.Cast
 import Mathlib.Analysis.Analytic.OfScalars
-import Mathlib.Analysis.SpecificLimits.RCLike
 
 /-!
 # Exponential in a Banach algebra
@@ -389,7 +388,7 @@ theorem expSeries_radius_eq_top : (expSeries 𝕂 𝔸).radius = ∞ := by
       inv_div_inv, norm_mul, div_self this, norm_one, one_mul]
     apply norm_zero (E := 𝕂) ▸ Filter.Tendsto.norm
     apply (Filter.tendsto_add_atTop_iff_nat (f := fun n => (n : 𝕂)⁻¹) 1).mpr
-    exact RCLike.tendsto_inverse_atTop_nhds_zero_nat 𝕂
+    exact tendsto_inv_atTop_nhds_zero_nat
   · simp [this]
 
 theorem expSeries_radius_pos : 0 < (expSeries 𝕂 𝔸).radius := by

Mathlib/Analysis/PSeries.lean

@@ -148,7 +148,7 @@ theorem le_tsum_schlomilch (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f
 
 theorem le_tsum_condensed (hf : ∀ ⦃m n⦄, 0 < m → m ≤ n → f n ≤ f m) :
     ∑' k, f k ≤ f 0 + ∑' k : ℕ, 2 ^ k * f (2 ^ k) := by
-  rw [ENNReal.tsum_eq_iSup_nat' (Nat.tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]
+  rw [ENNReal.tsum_eq_iSup_nat' (tendsto_pow_atTop_atTop_of_one_lt _root_.one_lt_two)]
   refine iSup_le fun n => (Finset.le_sum_condensed hf n).trans ?_
   simp only [nsmul_eq_mul, Nat.cast_pow, Nat.cast_two]
   grw [ENNReal.sum_le_tsum]

Mathlib/Analysis/Real/Hyperreal.lean

@@ -185,7 +185,7 @@ theorem gt_of_tendsto_zero_of_neg {f : ℕ → ℝ} (hf : Tendsto f atTop (𝓝
   rw [← neg_neg r, coe_neg]; exact neg_lt_of_tendsto_zero_of_pos hf (neg_pos.mpr hr)
 
 theorem epsilon_lt_pos (x : ℝ) : 0 < x → ε < x :=
-  lt_of_tendsto_zero_of_pos tendsto_inverse_atTop_nhds_zero_nat
+  lt_of_tendsto_zero_of_pos tendsto_inv_atTop_nhds_zero_nat
 
 /-- Standard part predicate -/
 def IsSt (x : ℝ*) (r : ℝ) :=
@@ -581,7 +581,7 @@ theorem infinitesimal_of_tendsto_zero {f : ℕ → ℝ} (h : Tendsto f atTop (
   isSt_of_tendsto h
 
 theorem infinitesimal_epsilon : Infinitesimal ε :=
-  infinitesimal_of_tendsto_zero tendsto_inverse_atTop_nhds_zero_nat
+  infinitesimal_of_tendsto_zero tendsto_inv_atTop_nhds_zero_nat
 
 theorem not_real_of_infinitesimal_ne_zero (x : ℝ*) : Infinitesimal x → x ≠ 0 → ∀ r : ℝ, x ≠ r :=
   fun hi hx r hr =>

Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean

@@ -6,6 +6,7 @@ Authors: Michael Stoll
 import Mathlib.Analysis.Complex.Convex
 import Mathlib.Analysis.SpecialFunctions.Integrals.Basic
 import Mathlib.Analysis.Calculus.Deriv.Shift
+import Mathlib.Analysis.SpecificLimits.RCLike
 
 /-!
 # Estimates for the complex logarithm

Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Edward Watine
 -/
 import Mathlib.Analysis.Analytic.OfScalars
-import Mathlib.Analysis.SpecificLimits.RCLike
+import Mathlib.Analysis.RCLike.Basic
 
 /-!
 # Ordinary hypergeometric function in a Banach algebra
@@ -204,6 +204,6 @@ theorem ordinaryHypergeometricSeries_radius_eq_one
         (c + k) / (a + k) * ((1 + k) / (b + k)) := by field
   simp_rw [this]
   apply (mul_one (1 : 𝕂)) ▸ Filter.Tendsto.mul <;>
-  convert RCLike.tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero <;> simp
+  convert tendsto_add_mul_div_add_mul_atTop_nhds _ _ (1 : 𝕂) one_ne_zero <;> simp
 
 end RCLike

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -10,6 +10,7 @@ import Mathlib.Order.Iterate
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.InfiniteSum.Real
 import Mathlib.Topology.Instances.EReal.Lemmas
+import Mathlib.Topology.Instances.Rat
 
 /-!
 # A collection of specific limit computations
@@ -27,24 +28,32 @@ open Set Function Filter Finset Metric Topology Nat uniformity NNReal ENNReal
 
 variable {α : Type*} {β : Type*} {ι : Type*}
 
-theorem tendsto_inverse_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) :=
+theorem NNRat.tendsto_inv_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ (n : ℚ≥0)⁻¹) atTop (𝓝 0) :=
   tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop
 
-theorem tendsto_const_div_atTop_nhds_zero_nat (C : ℝ) :
-    Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
-  simpa only [mul_zero] using tendsto_const_nhds.mul tendsto_inverse_atTop_nhds_zero_nat
-
-theorem tendsto_one_div_atTop_nhds_zero_nat : Tendsto (fun n : ℕ ↦ 1 / (n : ℝ)) atTop (𝓝 0) :=
-  tendsto_const_div_atTop_nhds_zero_nat 1
+theorem NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜]
+    [Algebra ℚ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
+    Tendsto (algebraMap ℚ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℚ≥0)⁻¹) atTop (𝓝 0) := by
+  convert (continuous_algebraMap ℚ≥0 𝕜).continuousAt.tendsto.comp
+    tendsto_inv_atTop_nhds_zero_nat
+  rw [map_zero]
 
-theorem NNReal.tendsto_inverse_atTop_nhds_zero_nat :
-    Tendsto (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0) := by
-  rw [← NNReal.tendsto_coe]
-  exact _root_.tendsto_inverse_atTop_nhds_zero_nat
+theorem tendsto_inv_atTop_nhds_zero_nat {𝕜 : Type*} [DivisionSemiring 𝕜] [CharZero 𝕜]
+    [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
+    Tendsto (fun n : ℕ ↦ (n : 𝕜)⁻¹) atTop (𝓝 0) := by
+  convert NNRat.tendsto_algebraMap_inv_atTop_nhds_zero_nat 𝕜
+  simp
 
-theorem NNReal.tendsto_const_div_atTop_nhds_zero_nat (C : ℝ≥0) :
+theorem tendsto_const_div_atTop_nhds_zero_nat {𝕜 : Type*} [DivisionSemiring 𝕜] [CharZero 𝕜]
+    [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [ContinuousMul 𝕜] (C : 𝕜) :
     Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
-  simpa using tendsto_const_nhds.mul NNReal.tendsto_inverse_atTop_nhds_zero_nat
+  simpa only [mul_zero, div_eq_mul_inv] using
+    (tendsto_const_nhds (x := C)).mul tendsto_inv_atTop_nhds_zero_nat
+
+theorem tendsto_one_div_atTop_nhds_zero_nat {𝕜 : Type*} [DivisionSemiring 𝕜] [CharZero 𝕜]
+    [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
+    Tendsto (fun n : ℕ ↦ 1 / (n : 𝕜)) atTop (𝓝 0) := by
+  simp [tendsto_inv_atTop_nhds_zero_nat]
 
 theorem EReal.tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥) (h' : C ≠ ⊤) :
     Tendsto (fun n : ℕ ↦ C / n) atTop (𝓝 0) := by
@@ -54,30 +63,23 @@ theorem EReal.tendsto_const_div_atTop_nhds_zero_nat {C : EReal} (h : C ≠ ⊥)
   rw [this, ← coe_zero, tendsto_coe]
   exact _root_.tendsto_const_div_atTop_nhds_zero_nat C.toReal
 
-theorem tendsto_one_div_add_atTop_nhds_zero_nat :
-    Tendsto (fun n : ℕ ↦ 1 / ((n : ℝ) + 1)) atTop (𝓝 0) :=
-  suffices Tendsto (fun n : ℕ ↦ 1 / (↑(n + 1) : ℝ)) atTop (𝓝 0) by simpa
-  (tendsto_add_atTop_iff_nat 1).2 (_root_.tendsto_const_div_atTop_nhds_zero_nat 1)
-
-theorem NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜]
-    [Algebra ℝ≥0 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℝ≥0 𝕜] :
-    Tendsto (algebraMap ℝ≥0 𝕜 ∘ fun n : ℕ ↦ (n : ℝ≥0)⁻¹) atTop (𝓝 0) := by
-  convert (continuous_algebraMap ℝ≥0 𝕜).continuousAt.tendsto.comp
-    tendsto_inverse_atTop_nhds_zero_nat
+theorem tendsto_one_div_add_atTop_nhds_zero_nat {𝕜 : Type*} [DivisionSemiring 𝕜] [CharZero 𝕜]
+    [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] :
+    Tendsto (fun n : ℕ ↦ 1 / ((n : 𝕜) + 1)) atTop (𝓝 0) :=
+  suffices Tendsto (fun n : ℕ ↦ 1 / (↑(n + 1) : 𝕜)) atTop (𝓝 0) by simpa
+  (tendsto_add_atTop_iff_nat 1).2 tendsto_one_div_atTop_nhds_zero_nat
+
+theorem tendsto_algebraMap_inv_atTop_nhds_zero_nat {𝕜 : Type*} (A : Type*)
+    [Semifield 𝕜] [CharZero 𝕜] [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜]
+    [Semiring A] [Algebra 𝕜 A] [TopologicalSpace A] [ContinuousSMul 𝕜 A] :
+    Tendsto (algebraMap 𝕜 A ∘ fun n : ℕ ↦ (n : 𝕜)⁻¹) atTop (𝓝 0) := by
+  convert (continuous_algebraMap 𝕜 A).continuousAt.tendsto.comp tendsto_inv_atTop_nhds_zero_nat
   rw [map_zero]
 
-theorem tendsto_algebraMap_inverse_atTop_nhds_zero_nat (𝕜 : Type*) [Semiring 𝕜] [Algebra ℝ 𝕜]
-    [TopologicalSpace 𝕜] [ContinuousSMul ℝ 𝕜] :
-    Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ ↦ (n : ℝ)⁻¹) atTop (𝓝 0) :=
-  NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜
-
 /-- The limit of `n / (n + x)` is 1, for any constant `x` (valid in `ℝ` or any topological division
-algebra over `ℝ`, e.g., `ℂ`).
-
-TODO: introduce a typeclass saying that `1 / n` tends to 0 at top, making it possible to get this
-statement simultaneously on `ℚ`, `ℝ` and `ℂ`. -/
-theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [TopologicalSpace 𝕜]
-    [CharZero 𝕜] [Algebra ℝ 𝕜] [ContinuousSMul ℝ 𝕜] [IsTopologicalDivisionRing 𝕜] (x : 𝕜) :
+algebra over `ℚ≥0`, e.g., `ℂ`). -/
+theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionSemiring 𝕜] [TopologicalSpace 𝕜]
+    [CharZero 𝕜] [ContinuousSMul ℚ≥0 𝕜] [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜] (x : 𝕜) :
     Tendsto (fun n : ℕ ↦ (n : 𝕜) / (n + x)) atTop (𝓝 1) := by
   convert Tendsto.congr' ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn ↦ _)) _
   · exact fun n : ℕ ↦ 1 / (1 + x / n)
@@ -88,12 +90,28 @@ theorem tendsto_natCast_div_add_atTop {𝕜 : Type*} [DivisionRing 𝕜] [Topolo
     refine tendsto_const_nhds.div (tendsto_const_nhds.add ?_) (by simp)
     simp_rw [div_eq_mul_inv]
     refine tendsto_const_nhds.mul ?_
-    have := ((continuous_algebraMap ℝ 𝕜).tendsto _).comp tendsto_inverse_atTop_nhds_zero_nat
+    have := ((continuous_algebraMap ℚ≥0 𝕜).tendsto _).comp tendsto_inv_atTop_nhds_zero_nat
     rw [map_zero, Filter.tendsto_atTop'] at this
     refine Iff.mpr tendsto_atTop' ?_
     intros
     simp_all only [comp_apply, map_inv₀, map_natCast]
 
+theorem tendsto_add_mul_div_add_mul_atTop_nhds {𝕜 : Type*} [Semifield 𝕜] [CharZero 𝕜]
+    [TopologicalSpace 𝕜] [ContinuousSMul ℚ≥0 𝕜] [IsTopologicalSemiring 𝕜] [ContinuousInv₀ 𝕜]
+    (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) :
+    Tendsto (fun k : ℕ ↦ (a + c * k) / (b + d * k)) atTop (𝓝 (c / d)) := by
+  apply Filter.Tendsto.congr'
+  case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)
+  · refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
+    intro h hx
+    dsimp
+    field (discharger := norm_cast)
+  · apply Filter.Tendsto.div _ _ hd
+    all_goals
+      apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
+      apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
+      exact tendsto_inv_atTop_nhds_zero_nat
+
 /-- For any positive `m : ℕ`, `((n % m : ℕ) : ℝ) / (n : ℝ)` tends to `0` as `n` tends to `∞`. -/
 theorem tendsto_mod_div_atTop_nhds_zero_nat {m : ℕ} (hm : 0 < m) :
     Tendsto (fun n : ℕ => ((n % m : ℕ) : ℝ) / (n : ℝ)) atTop (𝓝 0) := by
@@ -117,7 +135,7 @@ theorem Filter.EventuallyEq.div_mul_cancel {α G : Type*} [GroupWithZero G] {f g
 
 /-- If `g` tends to `∞`, then eventually for all `x` we have `(f x / g x) * g x = f x`. -/
 theorem Filter.EventuallyEq.div_mul_cancel_atTop {α K : Type*}
-    [Semifield K] [LinearOrder K] [IsStrictOrderedRing K]
+    [DivisionSemiring K] [LinearOrder K] [IsStrictOrderedRing K]
     {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) :
     (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x :=
   div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <|
@@ -163,16 +181,14 @@ theorem tendsto_add_one_pow_atTop_atTop_of_pos
     not_bddAbove_iff.2 fun _ ↦ Set.exists_range_iff.2 <| add_one_pow_unbounded_of_pos _ h
 
 theorem tendsto_pow_atTop_atTop_of_one_lt
-    [Ring α] [LinearOrder α] [IsStrictOrderedRing α] [Archimedean α] {r : α}
-    (h : 1 < r) : Tendsto (fun n : ℕ ↦ r ^ n) atTop atTop :=
-  sub_add_cancel r 1 ▸ tendsto_add_one_pow_atTop_atTop_of_pos (sub_pos.2 h)
-
-theorem Nat.tendsto_pow_atTop_atTop_of_one_lt {m : ℕ} (h : 1 < m) :
-    Tendsto (fun n : ℕ ↦ m ^ n) atTop atTop :=
-  tsub_add_cancel_of_le (le_of_lt h) ▸ tendsto_add_one_pow_atTop_atTop_of_pos (tsub_pos_of_lt h)
+    [Semiring α] [LinearOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α] [Archimedean α] {r : α}
+    (h : 1 < r) : Tendsto (fun n : ℕ ↦ r ^ n) atTop atTop := by
+  obtain ⟨r, r0, rfl⟩ := exists_pos_add_of_lt' h
+  rw [add_comm]
+  exact tendsto_add_one_pow_atTop_atTop_of_pos r0
 
 theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type*}
-    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [Archimedean 𝕜]
+    [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜] [Archimedean 𝕜]
     [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 ≤ r) (h₂ : r < 1) :
     Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
   h₁.eq_or_lt.elim
@@ -201,7 +217,7 @@ theorem tendsto_pow_atTop_nhds_zero_of_lt_one {𝕜 : Type*}
   · simpa only [← abs_pow] using (tendsto_pow_atTop_nhds_zero_of_lt_one (abs_nonneg r)) h
 
 theorem tendsto_pow_atTop_nhdsWithin_zero_of_lt_one {𝕜 : Type*}
-    [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
+    [Semifield 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] [ExistsAddOfLE 𝕜]
     [Archimedean 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] {r : 𝕜} (h₁ : 0 < r) (h₂ : r < 1) :
     Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝[>] 0) :=
   tendsto_inf.2
@@ -743,3 +759,23 @@ lemma Nat.tendsto_div_const_atTop {n : ℕ} (hn : n ≠ 0) : Tendsto (· / n) at
   rw [Tendsto, map_div_atTop_eq_nat n hn.bot_lt]
 
 end
+
+@[deprecated (since := "2025-10-27")]
+alias tendsto_inverse_atTop_nhds_zero_nat := tendsto_inv_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+alias NNReal.tendsto_inverse_atTop_nhds_zero_nat := tendsto_inv_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+alias NNReal.tendsto_const_div_atTop_nhds_zero_nat := tendsto_const_div_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+alias NNReal.tendsto_algebraMap_inverse_atTop_nhds_zero_nat :=
+  tendsto_algebraMap_inv_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+alias tendsto_algebraMap_inverse_atTop_nhds_zero_nat :=
+  tendsto_algebraMap_inv_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+protected alias Nat.tendsto_pow_atTop_atTop_of_one_lt := tendsto_pow_atTop_atTop_of_one_lt

Mathlib/Analysis/SpecificLimits/RCLike.lean

@@ -18,11 +18,6 @@ namespace RCLike
 
 variable (𝕜 : Type*) [RCLike 𝕜]
 
-theorem tendsto_inverse_atTop_nhds_zero_nat :
-    Tendsto (fun n : ℕ => (n : 𝕜)⁻¹) atTop (𝓝 0) := by
-  convert tendsto_algebraMap_inverse_atTop_nhds_zero_nat 𝕜
-  simp
-
 theorem tendsto_ofReal_cobounded_cobounded :
     Tendsto ofReal (Bornology.cobounded ℝ) (Bornology.cobounded 𝕜) :=
   tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_norm_cobounded_atTop)
@@ -35,19 +30,10 @@ theorem tendsto_ofReal_atBot_cobounded :
     Tendsto ofReal atBot (Bornology.cobounded 𝕜) :=
   tendsto_norm_atTop_iff_cobounded.mp (mod_cast tendsto_abs_atBot_atTop)
 
-variable {𝕜}
-
-theorem tendsto_add_mul_div_add_mul_atTop_nhds (a b c : 𝕜) {d : 𝕜} (hd : d ≠ 0) :
-    Tendsto (fun k : ℕ ↦ (a + c * k) / (b + d * k)) atTop (𝓝 (c / d)) := by
-  apply Filter.Tendsto.congr'
-  case f₁ => exact fun k ↦ (a * (↑k)⁻¹ + c) / (b * (↑k)⁻¹ + d)
-  · refine (eventually_ne_atTop 0).mp (Eventually.of_forall ?_)
-    intro h hx
-    field (discharger := norm_cast)
-  · apply Filter.Tendsto.div _ _ hd
-    all_goals
-      apply zero_add (_ : 𝕜) ▸ Filter.Tendsto.add_const _ _
-      apply mul_zero (_ : 𝕜) ▸ Filter.Tendsto.const_mul _ _
-      exact tendsto_inverse_atTop_nhds_zero_nat 𝕜
-
 end RCLike
+
+@[deprecated (since := "2025-10-27")]
+alias RCLike.tendsto_inverse_atTop_nhds_zero_nat := tendsto_inv_atTop_nhds_zero_nat
+
+@[deprecated (since := "2025-10-27")]
+alias RCLike.tendsto_add_mul_div_add_mul_atTop_nhds := tendsto_add_mul_div_add_mul_atTop_nhds

Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

@@ -563,7 +563,7 @@ theorem translationNumber_eq_of_tendsto₀ {τ' : ℝ}
     (h : Tendsto (fun n : ℕ => f^[n] 0 / n) atTop (𝓝 τ')) : τ f = τ' :=
   f.translationNumber_eq_of_tendsto_aux <| by
     simpa [Function.comp_def, transnumAuxSeq_def, coe_pow] using
-      h.comp (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two)
+      h.comp (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)
 
 theorem translationNumber_eq_of_tendsto₀' {τ' : ℝ}
     (h : Tendsto (fun n : ℕ => f^[n + 1] 0 / (n + 1)) atTop (𝓝 τ')) : τ f = τ' :=