chore(Analysis/Asymptotics): remove unnecessary hypothesis from isEquivalent_of_tendsto_one (leanprover-community#34389)

The condition `∀ᶠ x in l, v x = 0 → u x = 0` in `isEquivalent_of_tendsto_one` can be proven from the other assumption, `Tendsto (u / v) l (𝓝 1)`. This PR proves that and removes the former condition.

Author: vasnesterov

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -201,14 +201,17 @@ theorem IsEquivalent.exists_eq_mul (huv : u ~[l] v) :
     ∃ (φ : α → β) (_ : Tendsto φ l (𝓝 1)), u =ᶠ[l] φ * v :=
   isEquivalent_iff_exists_eq_mul.mp huv
 
-theorem isEquivalent_of_tendsto_one (hz : ∀ᶠ x in l, v x = 0 → u x = 0)
-    (huv : Tendsto (u / v) l (𝓝 1)) : u ~[l] v := by
-  rw [isEquivalent_iff_exists_eq_mul]
-  exact ⟨u / v, huv, hz.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
-
-theorem isEquivalent_of_tendsto_one' (hz : ∀ x, v x = 0 → u x = 0) (huv : Tendsto (u / v) l (𝓝 1)) :
-    u ~[l] v :=
-  isEquivalent_of_tendsto_one (Eventually.of_forall hz) huv
+theorem isEquivalent_of_tendsto_one (huv : Tendsto (u / v) l (𝓝 1)) :
+    u ~[l] v := by
+  suffices ∀ᶠ x in l, v x = 0 → u x = 0 by
+    rw [isEquivalent_iff_exists_eq_mul]
+    exact ⟨u / v, huv, this.mono fun x hz' ↦ (div_mul_cancel_of_imp hz').symm⟩
+  by_contra! h
+  replace h : ∃ᶠ t in l, (u / v) t = 0 := h.mono fun x ⟨hv, hu⟩ ↦ by simp [hv]
+  simpa using tendsto_nhds_unique_of_frequently_eq (b := 0) huv tendsto_const_nhds h
+
+@[deprecated (since := "2026-01-26")] alias isEquivalent_of_tendsto_one' :=
+  isEquivalent_of_tendsto_one
 
 theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
     u ~[l] v ↔ Tendsto (u / v) l (𝓝 1) := by
@@ -221,7 +224,7 @@ theorem isEquivalent_iff_tendsto_one (hz : ∀ᶠ x in l, v x ≠ 0) :
     convert this.add key
     · simp
     · simp
-  · exact isEquivalent_of_tendsto_one (hz.mono fun x hnvz hz ↦ (hnvz hz).elim)
+  · exact isEquivalent_of_tendsto_one
 
 end NormedField
 

Mathlib/Analysis/Asymptotics/SpecificAsymptotics.lean

@@ -181,13 +181,11 @@ variable {R : Type*} [NormedField R] [LinearOrder R] [IsStrictOrderedRing R]
   [OrderTopology R] [FloorRing R]
 
 theorem Asymptotics.isEquivalent_nat_floor :
-    (fun (x : R) ↦ ↑⌊x⌋₊) ~[atTop] (fun x ↦ x) := by
-  refine isEquivalent_of_tendsto_one ?_ tendsto_nat_floor_div_atTop
-  filter_upwards with x hx using by rw [hx, Nat.floor_zero, Nat.cast_eq_zero]
+    (fun (x : R) ↦ ↑⌊x⌋₊) ~[atTop] (fun x ↦ x) :=
+  isEquivalent_of_tendsto_one tendsto_nat_floor_div_atTop
 
 theorem Asymptotics.isEquivalent_nat_ceil :
-    (fun (x : R) ↦ ↑⌈x⌉₊) ~[atTop] (fun x ↦ x) := by
-  refine isEquivalent_of_tendsto_one ?_ tendsto_nat_ceil_div_atTop
-  filter_upwards with x hx using by rw [hx, Nat.ceil_zero, Nat.cast_eq_zero]
+    (fun (x : R) ↦ ↑⌈x⌉₊) ~[atTop] (fun x ↦ x) :=
+  isEquivalent_of_tendsto_one tendsto_nat_ceil_div_atTop
 
 end NormedLinearOrderedField

Mathlib/Analysis/SpecialFunctions/Stirling.lean

@@ -234,14 +234,12 @@ theorem tendsto_stirlingSeq_sqrt_pi : Tendsto stirlingSeq atTop (𝓝 (√π)) :
 /-- **Stirling's Formula**, formulated in terms of `Asymptotics.IsEquivalent`. -/
 lemma factorial_isEquivalent_stirling :
     (fun n ↦ n ! : ℕ → ℝ) ~[atTop] fun n ↦ Real.sqrt (2 * n * π) * (n / exp 1) ^ n := by
-  refine Asymptotics.isEquivalent_of_tendsto_one ?_ ?_
-  · filter_upwards [eventually_ne_atTop 0] with n hn h
-    exact absurd h (by positivity)
-  · have : sqrt π ≠ 0 := by positivity
-    nth_rewrite 2 [← div_self this]
-    convert tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1
-    ext n
-    simp [field, stirlingSeq, mul_right_comm]
+  apply Asymptotics.isEquivalent_of_tendsto_one
+  have : sqrt π ≠ 0 := by positivity
+  nth_rewrite 2 [← div_self this]
+  convert tendsto_stirlingSeq_sqrt_pi.div tendsto_const_nhds this using 1
+  ext n
+  simp [field, stirlingSeq, mul_right_comm]
 
 /-! ### Global bounds -/