chore: unused arguments (#17348)

Author: kim-em

Mathlib/Algebra/Algebra/Basic.lean

@@ -479,8 +479,8 @@ def LinearMap.extendScalarsOfSurjectiveEquiv (h : Function.Surjective (algebraMa
   map_add' _ _ := rfl
   map_smul' _ _ := rfl
   invFun f := f.restrictScalars S
-  left_inv f := rfl
-  right_inv f := rfl
+  left_inv _ := rfl
+  right_inv _ := rfl
 
 /-- If `R →+* S` is surjective, then `R`-linear maps are also `S`-linear. -/
 abbrev LinearMap.extendScalarsOfSurjective (h : Function.Surjective (algebraMap R S))

Mathlib/Algebra/Algebra/Equiv.lean

@@ -625,10 +625,10 @@ end OfRingEquiv
 -- @[simps (config := .lemmasOnly) one]
 instance aut : Group (A₁ ≃ₐ[R] A₁) where
   mul ϕ ψ := ψ.trans ϕ
-  mul_assoc ϕ ψ χ := rfl
+  mul_assoc _ _ _ := rfl
   one := refl
-  one_mul ϕ := ext fun x => rfl
-  mul_one ϕ := ext fun x => rfl
+  one_mul _ := ext fun _ => rfl
+  mul_one _ := ext fun _ => rfl
   inv := symm
   inv_mul_cancel ϕ := ext <| symm_apply_apply ϕ
 

Mathlib/Algebra/Algebra/Hom.lean

@@ -354,10 +354,10 @@ protected theorem map_list_prod (s : List A) : φ s.prod = (s.map φ).prod :=
 @[simps (config := .lemmasOnly) toSemigroup_toMul_mul toOne_one]
 instance End : Monoid (A →ₐ[R] A) where
   mul := comp
-  mul_assoc ϕ ψ χ := rfl
+  mul_assoc _ _ _ := rfl
   one := AlgHom.id R A
-  one_mul ϕ := rfl
-  mul_one ϕ := rfl
+  one_mul _ := rfl
+  mul_one _ := rfl
 
 @[simp]
 theorem one_apply (x : A) : (1 : A →ₐ[R] A) x = x :=

Mathlib/Algebra/Algebra/Operations.lean

@@ -490,10 +490,10 @@ submodules. -/
 def equivOpposite : Submodule R Aᵐᵒᵖ ≃+* (Submodule R A)ᵐᵒᵖ where
   toFun p := op <| p.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ)
   invFun p := p.unop.comap (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A)
-  left_inv p := SetLike.coe_injective <| rfl
-  right_inv p := unop_injective <| SetLike.coe_injective rfl
+  left_inv _ := SetLike.coe_injective <| rfl
+  right_inv _ := unop_injective <| SetLike.coe_injective rfl
   map_add' p q := by simp [comap_equiv_eq_map_symm, ← op_add]
-  map_mul' p q := congr_arg op <| comap_op_mul _ _
+  map_mul' _ _ := congr_arg op <| comap_op_mul _ _
 
 protected theorem map_pow {A'} [Semiring A'] [Algebra R A'] (f : A →ₐ[R] A') (n : ℕ) :
     map f.toLinearMap (M ^ n) = map f.toLinearMap M ^ n :=
@@ -647,7 +647,7 @@ theorem mem_div_iff_smul_subset {x : A} {I J : Submodule R A} : x ∈ I / J ↔
   ⟨fun h y ⟨y', hy', xy'_eq_y⟩ => by
     rw [← xy'_eq_y]
     apply h
-    assumption, fun h y hy => h (Set.smul_mem_smul_set hy)⟩
+    assumption, fun h _ hy => h (Set.smul_mem_smul_set hy)⟩
 
 theorem le_div_iff {I J K : Submodule R A} : I ≤ J / K ↔ ∀ x ∈ I, ∀ z ∈ K, x * z ∈ J :=
   Iff.refl _

Mathlib/Algebra/Algebra/Opposite.lean

@@ -38,7 +38,7 @@ variable [IsScalarTower R S A]
 namespace MulOpposite
 
 instance instAlgebra : Algebra R Aᵐᵒᵖ where
-  toRingHom := (algebraMap R A).toOpposite fun x y => Algebra.commutes _ _
+  toRingHom := (algebraMap R A).toOpposite fun _ _ => Algebra.commutes _ _
   smul_def' c x := unop_injective <| by
     simp only [unop_smul, RingHom.toOpposite_apply, Function.comp_apply, unop_mul, op_mul,
       Algebra.smul_def, Algebra.commutes, op_unop, unop_op]

Mathlib/Algebra/Algebra/Subalgebra/Basic.lean

@@ -280,8 +280,8 @@ instance (priority := 500) algebra' [CommSemiring R'] [SMul R' R] [Algebra R' A]
         Algebra.algebraMap_eq_smul_one]
       exact algebraMap_mem S
           _ with
-    commutes' := fun c x => Subtype.eq <| Algebra.commutes _ _
-    smul_def' := fun c x => Subtype.eq <| Algebra.smul_def _ _ }
+    commutes' := fun _ _ => Subtype.eq <| Algebra.commutes _ _
+    smul_def' := fun _ _ => Subtype.eq <| Algebra.smul_def _ _ }
 
 instance algebra : Algebra R S := S.algebra'
 

Mathlib/Algebra/Algebra/Tower.lean

@@ -265,7 +265,7 @@ open IsScalarTower
 
 theorem smul_mem_span_smul_of_mem {s : Set S} {t : Set A} {k : S} (hks : k ∈ span R s) {x : A}
     (hx : x ∈ t) : k • x ∈ span R (s • t) :=
-  span_induction hks (fun c hc => subset_span <| Set.smul_mem_smul hc hx)
+  span_induction hks (fun _ hc => subset_span <| Set.smul_mem_smul hc hx)
     (by rw [zero_smul]; exact zero_mem _)
     (fun c₁ c₂ ih₁ ih₂ => by rw [add_smul]; exact add_mem ih₁ ih₂)
     fun b c hc => by rw [IsScalarTower.smul_assoc]; exact smul_mem _ _ hc
@@ -274,7 +274,7 @@ theorem span_smul_of_span_eq_top {s : Set S} (hs : span R s = ⊤) (t : Set A) :
     span R (s • t) = (span S t).restrictScalars R :=
   le_antisymm
     (span_le.2 fun _x ⟨p, _hps, _q, hqt, hpqx⟩ ↦ hpqx ▸ (span S t).smul_mem p (subset_span hqt))
-    fun p hp ↦ closure_induction hp (zero_mem _) (fun _ _ ↦ add_mem) fun s0 y hy ↦ by
+    fun _ hp ↦ closure_induction hp (zero_mem _) (fun _ _ ↦ add_mem) fun s0 y hy ↦ by
       refine span_induction (hs ▸ mem_top : s0 ∈ span R s)
         (fun x hx ↦ subset_span ⟨x, hx, y, hy, rfl⟩) ?_ ?_ ?_
       · rw [zero_smul]; apply zero_mem

Mathlib/Algebra/Algebra/ZMod.lean

@@ -32,7 +32,7 @@ abbrev algebra' (h : m ∣ n) : Algebra (ZMod n) R :=
         rcases ZMod.intCast_surjective a with ⟨k, rfl⟩
         show ZMod.castHom h R k * r = r * ZMod.castHom h R k
         rw [map_intCast, Int.cast_comm]
-    smul_def' := fun a r => rfl }
+    smul_def' := fun _ _ => rfl }
 
 end
 

Mathlib/Algebra/Associated/Basic.lean

@@ -831,7 +831,7 @@ instance instCommMonoid : CommMonoid (Associates M) where
 instance instPreorder : Preorder (Associates M) where
   le := Dvd.dvd
   le_refl := dvd_refl
-  le_trans a b c := dvd_trans
+  le_trans _ _ _ := dvd_trans
 
 /-- `Associates.mk` as a `MonoidHom`. -/
 protected def mkMonoidHom : M →* Associates M where

Mathlib/Algebra/BigOperators/Associated.lean

@@ -187,7 +187,7 @@ variable [CancelCommMonoidWithZero α]
 
 theorem exists_mem_multiset_le_of_prime {s : Multiset (Associates α)} {p : Associates α}
     (hp : Prime p) : p ≤ s.prod → ∃ a ∈ s, p ≤ a :=
-  Multiset.induction_on s (fun ⟨d, Eq⟩ => (hp.ne_one (mul_eq_one.1 Eq.symm).1).elim)
+  Multiset.induction_on s (fun ⟨_, Eq⟩ => (hp.ne_one (mul_eq_one.1 Eq.symm).1).elim)
     fun a s ih h =>
     have : p ≤ a * s.prod := by simpa using h
     match Prime.le_or_le hp this with