chore(Analysis): remove unused variables (#17874)

These were already unused on the master branch but became exposed to the linter after #17870 changed some `CoeFun` instances.
leanprover-community · Oct 17, 2024 · d2ce997 · d2ce997
1 parent e007f8f
commit d2ce997
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git a/Mathlib/Analysis/Analytic/Basic.lean b/Mathlib/Analysis/Analytic/Basic.lean
@@ -638,7 +638,7 @@ theorem HasFPowerSeriesWithinOnBall.coeff_zero (hf : HasFPowerSeriesWithinOnBall
     (v : Fin 0 → E) : pf 0 v = f x := by
   have v_eq : v = fun i => 0 := Subsingleton.elim _ _
   have zero_mem : (0 : E) ∈ EMetric.ball (0 : E) r := by simp [hf.r_pos]
-  have : ∀ i, i ≠ 0 → (pf i fun j => 0) = 0 := by
+  have : ∀ i, i ≠ 0 → (pf i fun _ => 0) = 0 := by
     intro i hi
     have : 0 < i := pos_iff_ne_zero.2 hi
     exact ContinuousMultilinearMap.map_coord_zero _ (⟨0, this⟩ : Fin i) rfl

diff --git a/Mathlib/Analysis/Analytic/Inverse.lean b/Mathlib/Analysis/Analytic/Inverse.lean
@@ -272,7 +272,7 @@ theorem rightInv_coeff (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜]
     congr (config := { closePost := false }) 1
     ext v
     have N : 0 < n + 2 := by norm_num
-    have : ((p 1) fun i : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
+    have : ((p 1) fun _ : Fin 1 => 0) = 0 := ContinuousMultilinearMap.map_zero _
     simp [comp_rightInv_aux1 N, lt_irrefl n, this, comp_rightInv_aux2, -Set.toFinset_setOf]
 
 /-! ### Coincidence of the left and the right inverse -/
@@ -630,10 +630,10 @@ lemma HasFPowerSeriesAt.eventually_hasSum_of_comp  {f : E → F} {g : F → G}
     simp only [id_eq, eventually_atTop, ge_iff_le]
     rcases mem_nhds_iff.1 hu with ⟨v, vu, v_open, hv⟩
     obtain ⟨a₀, b₀, hab⟩ : ∃ a₀ b₀, ∀ (a b : ℕ), a₀ ≤ a → b₀ ≤ b →
-        q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0) ∈ v := by
+        q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0) ∈ v := by
       simpa using hy (v_open.mem_nhds hv)
     refine ⟨a₀, fun a ha ↦ ?_⟩
-    have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun x ↦ 0)) atTop
+    have : Tendsto (fun b ↦ q.partialSum a (p.partialSum b y - (p 0) fun _ ↦ 0)) atTop
         (𝓝 (q.partialSum a (f (x + y) - f x))) := by
       have : ContinuousAt (q.partialSum a) (f (x + y) - f x) :=
         (partialSum_continuous q a).continuousAt

diff --git a/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean b/Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
@@ -166,7 +166,7 @@ theorem iteratedDerivWithin_succ {x : 𝕜} (hxs : UniqueDiffWithinAt 𝕜 s x)
   rw [iteratedDerivWithin_eq_iteratedFDerivWithin, iteratedFDerivWithin_succ_apply_left,
     iteratedFDerivWithin_eq_equiv_comp, LinearIsometryEquiv.comp_fderivWithin _ hxs, derivWithin]
   change ((ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) ((fderivWithin 𝕜
-    (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun i : Fin n => 1) =
+    (iteratedDerivWithin n f s) s x : 𝕜 → F) 1) : (Fin n → 𝕜) → F) fun _ : Fin n => 1) =
     (fderivWithin 𝕜 (iteratedDerivWithin n f s) s x : 𝕜 → F) 1
   simp
 

diff --git a/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean b/Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
@@ -115,7 +115,7 @@ variable [T2Space R] [T2Space M]
 theorem exp_def_of_smul_comm (x : tsze R M) (hx : MulOpposite.op x.fst • x.snd = x.fst • x.snd) :
     exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) := by
   simp_rw [exp, FormalMultilinearSeries.sum]
-  by_cases h : Summable (fun (n : ℕ) => (expSeries 𝕜 R n) fun x_1 ↦ fst x)
+  by_cases h : Summable (fun (n : ℕ) => (expSeries 𝕜 R n) fun _ ↦ fst x)
   · refine (hasSum_expSeries_of_smul_comm 𝕜 x hx ?_).tsum_eq
     exact h.hasSum
   · rw [tsum_eq_zero_of_not_summable h, zero_smul, inr_zero, inl_zero, zero_add,