feat(Topology/Separation/Hausdorff): add tendsto_nhds_unique_of_forall

Counterexamples/TopologistsSineCurve.lean

@@ -85,8 +85,7 @@ lemma closure_S : closure S = T := by
       simp only [Prod.mk.injEq, true_and]
       have : ContinuousAt (fun x ↦ sin x⁻¹) x :=
         continuous_sin.continuousAt.comp <| continuousAt_inv₀ h.ne'
-      refine tendsto_nhds_unique ?_ hf_lim.2
-      convert! this.tendsto.comp hf_lim.1 with n
+      refine tendsto_nhds_unique_of_forall (this.tendsto.comp hf_lim.1) hf_lim.2 fun n ↦ ?_
       obtain ⟨y, hy⟩ := hf_mem n
       simp [← hy.2]
   · -- Show that every `p ∈ T` is the limit of a sequence in `S`.

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Continuity.lean

@@ -614,9 +614,8 @@ theorem tendsto_cfcₙ_fun {l : Filter X} {F : X → R → R} {f : R → R} {a :
   obtain (rfl | hl) := l.eq_or_neBot
   · simp
   have hf := h_tendsto.continuousOn hF.frequently
-  have hf0 : f 0 = 0 := Eq.symm <|
-    tendsto_nhds_unique (tendsto_const_nhds.congr' <| .symm hF0) <|
-    h_tendsto.tendsto_at (quasispectrum.zero_mem R a)
+  have hf0 : f 0 = 0 := tendsto_nhds_unique_of_eventuallyEq
+    (h_tendsto.tendsto_at (quasispectrum.zero_mem R a)) tendsto_const_nhds hF0
   by_cases ha : p a
   · let s : Set X := {x | ContinuousOn (F x) (quasispectrum R a) ∧ F x 0 = 0}
     have hs : s ∈ l := hF.and hF0

Mathlib/Analysis/CStarAlgebra/Spectrum.lean

@@ -117,11 +117,8 @@ local notation "↑ₐ" => algebraMap ℂ A
 theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {a : A} (ha : IsSelfAdjoint a) :
     spectralRadius ℂ a = ‖a‖₊ := by
   have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds
-  refine tendsto_nhds_unique ?_ hconst
-  convert!
-    (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
-      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1
-  refine funext fun n => ?_
+  refine tendsto_nhds_unique_of_forall ((pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius a).comp
+      (tendsto_pow_atTop_atTop_of_one_lt one_lt_two)) hconst fun n ↦ ?_
   rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]
   simp
 

Mathlib/Analysis/Complex/Liouville.lean

@@ -143,7 +143,7 @@ theorem eq_const_of_tendsto_cocompact [Nontrivial E] {f : E → F} (hf : Differe
       _        ⊆ t ∪ s  := by gcongr
   obtain ⟨c', hc'⟩ := hf.exists_eq_const_of_bounded h_bdd
   convert hc'
-  exact tendsto_nhds_unique hb (by simpa [hc'] using! tendsto_const_nhds)
+  exact tendsto_nhds_unique_of_forall hb tendsto_const_nhds (by simp [hc'])
 
 /-- A corollary of Liouville's theorem where the function tends to a finite value at infinity
 (i.e., along `Filter.cocompact`, which in proper spaces coincides with `Bornology.cobounded`). -/

Mathlib/Analysis/InnerProductSpace/l2Space.lean

@@ -201,12 +201,11 @@ protected def linearIsometry (hV : OrthogonalFamily 𝕜 G V) : lp G 2 →ₗᵢ
   norm_map' f := by
     -- needed for lattice instance on `Finset ι`, for `Filter.atTop_neBot`
     have H : 0 < (2 : ℝ≥0∞).toReal := by simp
-    suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal by
-      exact Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
-    refine tendsto_nhds_unique ?_ (lp.hasSum_norm H f)
-    convert! (hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le) using 1
-    ext s
-    exact mod_cast (hV.norm_sum f s).symm
+    suffices ‖∑' i : ι, V i (f i)‖ ^ (2 : ℝ≥0∞).toReal = ‖f‖ ^ (2 : ℝ≥0∞).toReal from
+      Real.rpow_left_injOn H.ne' (norm_nonneg _) (norm_nonneg _) this
+    exact tendsto_nhds_unique_of_forall
+      ((hV.summable_of_lp f).hasSum.norm.rpow_const (Or.inr H.le)) (lp.hasSum_norm H f)
+      fun s ↦ mod_cast (hV.norm_sum f s)
 
 protected theorem linearIsometry_apply (f : lp G 2) : hV.linearIsometry f = ∑' i, V i (f i) :=
   rfl

Mathlib/Analysis/Normed/Unbundled/SeminormFromConst.lean

@@ -185,9 +185,8 @@ theorem seminormFromConst_isPowMul : IsPowMul (seminormFromConst' c f) := fun x
     apply (tendsto_seminormFromConst_seq_atTop hc hpm (x ^ m)).comp
       (tendsto_atTop_atTop_of_monotone (fun _ _ hnk ↦ mul_le_mul_right hnk m) _)
     rintro n; use n; exact le_mul_of_one_le_left' hm
-  apply tendsto_nhds_unique hlim
-  convert! (tendsto_seminormFromConst_seq_atTop hc hpm x).pow m using 1
-  ext n
+  refine tendsto_nhds_unique_of_forall hlim
+    ((tendsto_seminormFromConst_seq_atTop hc hpm x).pow m) fun n ↦ ?_
   simp only [seminormFromConst_seq, div_pow, ← hpm _ hm, ← pow_mul, mul_pow, mul_comm m n]
 
 /-- The function `seminormFromConst' c f` is bounded above by `f`. -/

Mathlib/Analysis/SpecialFunctions/ArithmeticGeometricMean.lean

@@ -242,10 +242,9 @@ lemma agm_pos (hx : 0 < x) (hy : 0 < y) : 0 < agm x y := (lt_min hx hy).trans_le
 
 lemma agm_eq_agm_agmSequences_fst_agmSequences_snd (n : ℕ) :
     agm x y = agm (agmSequences x y n).1 (agmSequences x y n).2 := by
-  refine tendsto_nhds_unique ?_ tendsto_agmSequences_snd_agm
   have key := @tendsto_agmSequences_snd_agm x y
   rw [← tendsto_add_atTop_iff_nat (n + 1)] at key
-  convert! key using 2 with m
+  refine tendsto_nhds_unique_of_forall key tendsto_agmSequences_snd_agm fun m ↦ ?_
   simp_rw [agmSequences, Prod.mk.eta, ← iterate_add_apply, add_right_comm]
 
 lemma agm_eq_agm_gm_am : agm x y = agm (sqrt (x * y)) ((x + y) / 2) := by

Mathlib/MeasureTheory/Integral/CircleAverage.lean

@@ -232,8 +232,8 @@ lemma ContinuousOn.eq_of_eqOn_Ioo {f : ℝ → ℝ} {c r R : ℝ}
     rw [nhdsWithin_le_iff, mem_nhdsLT_iff_exists_Ioo_subset]
     use r
     simp_all [Ioo_subset_Ioc_self]
-  apply tendsto_nhds_unique this (tendsto_const_nhds.congr' _)
-  apply Filter.eventuallyEq_of_mem (Ioo_mem_nhdsLT hR) (fun _ hx ↦ (h₂f hx).symm)
+  refine tendsto_nhds_unique_of_eventuallyEq this tendsto_const_nhds ?_
+  exact Filter.eventuallyEq_of_mem (Ioo_mem_nhdsLT hR) h₂f
 
 /-!
 ## Constant Functions

Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

@@ -792,11 +792,10 @@ theorem integral_Ioi_of_hasDerivAt_of_tendsto (hcont : ContinuousWithinAt f (Ici
     rcases hx.out.eq_or_lt with rfl | hx
     · exact hcont
     · exact (hderiv x hx).continuousAt.continuousWithinAt
-  refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) ?_
-  apply Tendsto.congr' _ (hf.sub_const _)
+  refine tendsto_nhds_unique_of_eventuallyEq
+    (intervalIntegral_tendsto_integral_Ioi a f'int tendsto_id) (hf.sub_const _) ?_
   filter_upwards [Ioi_mem_atTop a] with x hx
   have h'x : a ≤ id x := le_of_lt hx
-  symm
   apply
     intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le h'x (hcont.mono Icc_subset_Ici_self)
       fun y hy => hderiv y hy.1
@@ -989,10 +988,9 @@ theorem integral_Iic_of_hasDerivAt_of_tendsto (hcont : ContinuousWithinAt f (Iic
     rcases hx.out.eq_or_lt with rfl | hx
     · exact hcont
     · exact (hderiv x hx).continuousAt.continuousWithinAt
-  refine tendsto_nhds_unique (intervalIntegral_tendsto_integral_Iic a f'int tendsto_id) ?_
-  apply Tendsto.congr' _ (hf.const_sub _)
+  refine tendsto_nhds_unique_of_eventuallyEq
+    (intervalIntegral_tendsto_integral_Iic a f'int tendsto_id) (hf.const_sub _) ?_
   filter_upwards [Iic_mem_atBot a] with x hx
-  symm
   apply intervalIntegral.integral_eq_sub_of_hasDerivAt_of_le hx
     (hcont.mono Icc_subset_Iic_self) fun y hy => hderiv y hy.2
   rw [intervalIntegrable_iff_integrableOn_Ioc_of_le hx]
@@ -1112,7 +1110,7 @@ theorem integral_deriv_smul_comp_Ioi {f f' : ℝ → ℝ} {g : ℝ → E} {a : 
       IsPreconnected.intermediate_value_Ici isPreconnected_Ici self_mem_Ici
         (le_principal_iff.mpr <| Ici_mem_atTop _) hf hft
   have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
-  exact tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1
+  exact tendsto_nhds_unique_of_eventuallyEq t2 t1 (eventuallyEq_of_mem (Ioi_mem_atTop a) eq)
 
 @[deprecated (since := "2026-03-19")]
 alias integral_comp_smul_deriv_Ioi := integral_deriv_smul_comp_Ioi

Mathlib/MeasureTheory/Integral/SetToL1.lean

@@ -968,13 +968,10 @@ theorem setToFun_of_le_map_of_stronglyMeasurable
     ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hf).mono_measure hμ'
   borelize E
   have : SeparableSpace (range f ∪ {0} : Set E) := hfm.separableSpace_range_union_singleton
-  refine tendsto_nhds_unique
-    (tendsto_setToFun_approxOn_of_measurable_of_range_subset
-      hT' hfm.measurable hfi' _ Subset.rfl) ?_
-  convert tendsto_setToFun_approxOn_of_measurable_of_range_subset
-    hT (hfm.measurable.comp hφ) hf (range f ∪ {0})
-    (union_subset_union_left {0} (range_comp_subset_range φ f)) using 1
-  ext i : 1
+  refine tendsto_nhds_unique_of_forall
+    (tendsto_setToFun_approxOn_of_measurable_of_range_subset hT' hfm.measurable hfi' _ Subset.rfl)
+      (tendsto_setToFun_approxOn_of_measurable_of_range_subset hT (hfm.measurable.comp hφ) hf
+        (range f ∪ {0}) (union_subset_union_left {0} (range_comp_subset_range φ f))) fun i ↦ ?_
   rw [setToFun_simpleFunc _ _ (SimpleFunc.integrable_approxOn_range _ hfi' _),
     setToFun_simpleFunc, SimpleFunc.approxOn_comp hfm.measurable hφ]; swap
   · apply SimpleFunc.integrable_approxOn _ hf (by simp) (by simp)

Mathlib/MeasureTheory/Measure/Stieltjes.lean

@@ -618,9 +618,8 @@ theorem measure_Iic {l : ℝ} (hf : Tendsto f atBot (𝓝 l)) (x : R) :
     rw [this, measure_Icc, leftLim_eq_of_isBot isBot_bot,
       tendsto_nhds_unique hf (tendsto_pure_nhds f ⊥)]
   have : NoMinOrder R := NoBotOrder.to_noMinOrder R
-  refine tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) ?_
-  simp_rw [measure_Ioc]
-  exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)
+  exact tendsto_nhds_unique_of_forall (tendsto_measure_Ioc_atBot _ _)
+    (ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)) (by simp)
 
 lemma measure_Iio {l : ℝ} (hf : Tendsto f atBot (𝓝 l)) (x : R) :
     f.measure (Iio x) = ofReal (leftLim f x - l) := by
@@ -637,9 +636,8 @@ theorem measure_Ici {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : R) :
     rw [atTop_eq_pure_of_isTop isTop_top] at hf
     rw [this, measure_Icc, tendsto_nhds_unique hf (tendsto_pure_nhds f ⊤)]
   have : NoMaxOrder R := NoTopOrder.to_noMaxOrder R
-  refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_
-  simp_rw [measure_Ico]
-  exact ENNReal.tendsto_ofReal (Tendsto.sub_const (tendsto_leftLim_atTop_of_tendsto hf) _)
+  exact tendsto_nhds_unique_of_forall (tendsto_measure_Ico_atTop _ _)
+    (ENNReal.tendsto_ofReal (Tendsto.sub_const (tendsto_leftLim_atTop_of_tendsto hf) _)) (by simp)
 
 lemma measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : R) :
     f.measure (Ioi x) = ofReal (l - f x) := by
@@ -682,9 +680,8 @@ lemma measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : R) :
 theorem measure_univ [Nonempty R]
     {l u : ℝ} (hfl : Tendsto f atBot (𝓝 l)) (hfu : Tendsto f atTop (𝓝 u)) :
     f.measure univ = ofReal (u - l) := by
-  refine tendsto_nhds_unique (tendsto_measure_Iic_atTop _) ?_
-  simp_rw [measure_Iic f hfl]
-  exact ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)
+  exact tendsto_nhds_unique_of_forall (tendsto_measure_Iic_atTop _)
+    (ENNReal.tendsto_ofReal (Tendsto.sub_const hfu _)) (by simp [measure_Iic f hfl])
 
 lemma measure_univ_of_tendsto_atTop_atTop [Nonempty R] (hf : Tendsto f atTop atTop) :
     f.measure univ = ∞ := by

Mathlib/Topology/Separation/Hausdorff.lean

@@ -194,6 +194,10 @@ theorem tendsto_nhds_unique_of_frequently_eq [T2Space X] {f g : Y → X} {l : Fi
   have : ∃ᶠ z : X × X in 𝓝 (a, b), z.1 = z.2 := (ha.prodMk_nhds hb).frequently hfg
   not_not.1 fun hne => this (isClosed_diagonal.isOpen_compl.mem_nhds hne)
 
+theorem tendsto_nhds_unique_of_forall [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X}
+    [NeBot l] (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) (hfg : ∀ y, f y = g y) : a = b :=
+  tendsto_nhds_unique_of_eventuallyEq ha hb (Eventually.of_forall hfg)
+
 /-- If `s` and `t` are compact sets in a T₂ space, then the set neighborhoods filter of `s ∩ t`
 is the infimum of set neighborhoods filters for `s` and `t`.