chore(Topology/Basic): re-use variables; rename a : X to x : X (#9993)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

Author: 3 people

Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean

@@ -141,10 +141,10 @@ theorem isEquivalent_const_iff_tendsto {c : β} (h : c ≠ 0) :
     u ~[l] const _ c ↔ Tendsto u l (𝓝 c) := by
   simp (config := { unfoldPartialApp := true }) only [IsEquivalent, const, isLittleO_const_iff h]
   constructor <;> intro h
-  · have := h.sub (tendsto_const_nhds (a := -c))
+  · have := h.sub (tendsto_const_nhds (x := -c))
     simp only [Pi.sub_apply, sub_neg_eq_add, sub_add_cancel, zero_add] at this
     exact this
-  · have := h.sub (tendsto_const_nhds (a := c))
+  · have := h.sub (tendsto_const_nhds (x := c))
     rwa [sub_self] at this
 #align asymptotics.is_equivalent_const_iff_tendsto Asymptotics.isEquivalent_const_iff_tendsto
 

Mathlib/Analysis/Calculus/FDeriv/Basic.lean

@@ -779,7 +779,7 @@ theorem HasFDerivAtFilter.tendsto_nhds (hL : L ≤ 𝓝 x) (h : HasFDerivAtFilte
     refine' h.isBigO_sub.trans_tendsto (Tendsto.mono_left _ hL)
     rw [← sub_self x]
     exact tendsto_id.sub tendsto_const_nhds
-  have := this.add (@tendsto_const_nhds _ _ _ (f x) _)
+  have := this.add (tendsto_const_nhds (x := f x))
   rw [zero_add (f x)] at this
   exact this.congr (by simp only [sub_add_cancel, eq_self_iff_true, forall_const])
 #align has_fderiv_at_filter.tendsto_nhds HasFDerivAtFilter.tendsto_nhds

Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

@@ -216,7 +216,7 @@ variable (f)
 theorem tendsto_integral_exp_inner_smul_cocompact :
     Tendsto (fun w : V => ∫ v, e[-⟪v, w⟫] • f v) (cocompact V) (𝓝 0) := by
   by_cases hfi : Integrable f; swap
-  · convert tendsto_const_nhds (a := (0 : E)) with w
+  · convert tendsto_const_nhds (x := (0 : E)) with w
     apply integral_undef
     rwa [← fourier_integrand_integrable w]
   refine' Metric.tendsto_nhds.mpr fun ε hε => _

Mathlib/Analysis/InnerProductSpace/Projection.lean

@@ -172,10 +172,10 @@ theorem exists_norm_eq_iInf_of_complete_convex {K : Set F} (ne : K.Nonempty) (h
       convert this
       exact sqrt_zero.symm
     have eq₁ : Tendsto (fun n : ℕ => 8 * δ * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by
-      convert (@tendsto_const_nhds _ _ _ (8 * δ) _).mul tendsto_one_div_add_atTop_nhds_0_nat
+      convert (tendsto_const_nhds (x := 8 * δ)).mul tendsto_one_div_add_atTop_nhds_0_nat
       simp only [mul_zero]
     have : Tendsto (fun n : ℕ => (4 : ℝ) * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by
-      convert (@tendsto_const_nhds _ _ _ (4 : ℝ) _).mul tendsto_one_div_add_atTop_nhds_0_nat
+      convert (tendsto_const_nhds (x := 4)).mul tendsto_one_div_add_atTop_nhds_0_nat
       simp only [mul_zero]
     have eq₂ :
         Tendsto (fun n : ℕ => (4 : ℝ) * (1 / (n + 1)) * (1 / (n + 1))) atTop (nhds (0 : ℝ)) := by

Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean

@@ -1311,7 +1311,7 @@ instance completeSpace [CompleteSpace G] : CompleteSpace (ContinuousMultilinearM
       map_smul' := fun v i c x => by
         skip
         have A := hF (Function.update v i (c • x))
-        have B := Filter.Tendsto.smul (@tendsto_const_nhds _ ℕ _ c _) (hF (Function.update v i x))
+        have B := Filter.Tendsto.smul (tendsto_const_nhds (x := c)) (hF (Function.update v i x))
         simp? at A B says simp only [map_smul] at A B
         exact tendsto_nhds_unique A B }
   -- and that `F` has norm at most `(b 0 + ‖f 0‖)`.

Mathlib/Analysis/SpecialFunctions/Pow/Asymptotics.lean

@@ -108,7 +108,7 @@ theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) :
       ((tendsto_exp_nhds_0_nhds_1.comp
             (by
               simpa only [mul_zero, pow_one] using
-                (@tendsto_const_nhds _ _ _ a _).mul
+                (tendsto_const_nhds (x := a)).mul
                   (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
         tendsto_log_atTop)
   apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))

Mathlib/Topology/Algebra/Algebra.lean

@@ -111,7 +111,7 @@ theorem Subalgebra.le_topologicalClosure (s : Subalgebra R A) : s ≤ s.topologi
 #align subalgebra.le_topological_closure Subalgebra.le_topologicalClosure
 
 theorem Subalgebra.isClosed_topologicalClosure (s : Subalgebra R A) :
-    IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A _ s
+    IsClosed (s.topologicalClosure : Set A) := by convert @isClosed_closure A s _
 #align subalgebra.is_closed_topological_closure Subalgebra.isClosed_topologicalClosure
 
 theorem Subalgebra.topologicalClosure_minimal (s : Subalgebra R A) {t : Subalgebra R A} (h : s ≤ t)

Mathlib/Topology/Algebra/Order/LiminfLimsup.lean

@@ -183,7 +183,7 @@ set_option linter.uppercaseLean3 false in
 
 theorem limsSup_nhds (a : α) : limsSup (𝓝 a) = a :=
   csInf_eq_of_forall_ge_of_forall_gt_exists_lt (isBounded_le_nhds a)
-    (fun a' (h : { n : α | n ≤ a' } ∈ 𝓝 a) ↦ show a ≤ a' from @mem_of_mem_nhds α _ a _ h)
+    (fun a' (h : { n : α | n ≤ a' } ∈ 𝓝 a) ↦ show a ≤ a' from @mem_of_mem_nhds α a _ _ h)
     fun b (hba : a < b) ↦
     show ∃ c, { n : α | n ≤ c } ∈ 𝓝 a ∧ c < b from
       match dense_or_discrete a b with

Mathlib/Topology/Bases.lean

@@ -130,7 +130,7 @@ theorem isTopologicalBasis_of_isOpen_of_nhds {s : Set (Set α)} (h_open : ∀ u
     rcases h_nhds a univ trivial isOpen_univ with ⟨u, h₁, h₂, -⟩
     exact ⟨u, h₁, h₂⟩
   · refine' (le_generateFrom h_open).antisymm fun u hu => _
-    refine' (@isOpen_iff_nhds α (generateFrom s) u).mpr fun a ha => _
+    refine (@isOpen_iff_nhds α u (generateFrom s)).mpr fun a ha ↦ ?_
     rcases h_nhds a u ha hu with ⟨v, hvs, hav, hvu⟩
     rw [nhds_generateFrom]
     exact iInf₂_le_of_le v ⟨hav, hvs⟩ (le_principal_iff.2 hvu)