chore: cleanup simp calls (#9539)

Remove some unnecessary arguments in `simp` calls, which will become problematic when the `simp` algorithm changes in leanprover/lean4#3124.



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

Mathlib/Algebra/BigOperators/Fin.lean

@@ -230,7 +230,7 @@ theorem partialProd_zero (f : Fin n → α) : partialProd f 0 = 1 := by simp [pa
 @[to_additive]
 theorem partialProd_succ (f : Fin n → α) (j : Fin n) :
     partialProd f j.succ = partialProd f (Fin.castSucc j) * f j := by
-  simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt, ← Option.coe_def]
+  simp [partialProd, List.take_succ, List.ofFnNthVal, dif_pos j.is_lt]
 #align fin.partial_prod_succ Fin.partialProd_succ
 #align fin.partial_sum_succ Fin.partialSum_succ
 

Mathlib/Analysis/InnerProductSpace/l2Space.lean

@@ -415,16 +415,15 @@ instance {ι : Type*} : Inhabited (HilbertBasis ι 𝕜 ℓ²(ι, 𝕜)) :=
 instance instCoeFun : CoeFun (HilbertBasis ι 𝕜 E) fun _ => ι → E where
   coe b i := b.repr.symm (lp.single 2 i (1 : 𝕜))
 
-@[simp]
+-- This is a bad `@[simp]` lemma: the RHS is a coercion containing the LHS.
 protected theorem repr_symm_single (b : HilbertBasis ι 𝕜 E) (i : ι) :
     b.repr.symm (lp.single 2 i (1 : 𝕜)) = b i :=
   rfl
 #align hilbert_basis.repr_symm_single HilbertBasis.repr_symm_single
 
--- porting note: removed `@[simp]` because `simp` can prove this
 protected theorem repr_self (b : HilbertBasis ι 𝕜 E) (i : ι) :
     b.repr (b i) = lp.single 2 i (1 : 𝕜) := by
-  simp
+  simp only [LinearIsometryEquiv.apply_symm_apply]
 #align hilbert_basis.repr_self HilbertBasis.repr_self
 
 protected theorem repr_apply_apply (b : HilbertBasis ι 𝕜 E) (v : E) (i : ι) :

Mathlib/CategoryTheory/Limits/Opposites.lean

@@ -468,8 +468,8 @@ theorem desc_op_comp_opCoproductIsoProduct_hom {X : C} (π : (a : α) → Z a 
     (Sigma.desc π).op ≫ (opCoproductIsoProduct Z).hom = Pi.lift (fun a ↦ (π a).op) := by
   convert desc_op_comp_opCoproductIsoProduct'_hom (coproductIsCoproduct Z)
     (productIsProduct (op <| Z ·)) (Cofan.mk _ π)
-  · ext; simp [Sigma.desc, colimit.desc, coproductIsCoproduct]
-  · ext; simp [Pi.lift, limit.lift, productIsProduct]
+  · ext; simp [Sigma.desc, coproductIsCoproduct]
+  · ext; simp [Pi.lift, productIsProduct]
 
 end OppositeCoproducts
 
@@ -542,8 +542,8 @@ theorem opProductIsoCoproduct_inv_comp_lift {X : C} (π : (a : α) → X ⟶ Z a
     (opProductIsoCoproduct Z).inv ≫ (Pi.lift π).op  = Sigma.desc (fun a ↦ (π a).op) := by
   convert opProductIsoCoproduct'_inv_comp_lift (productIsProduct Z)
     (coproductIsCoproduct (op <| Z ·)) (Fan.mk _ π)
-  · ext; simp [Pi.lift, limit.lift, productIsProduct]
-  · ext; simp [Sigma.desc, colimit.desc, coproductIsCoproduct]
+  · ext; simp [Pi.lift, productIsProduct]
+  · ext; simp [Sigma.desc, coproductIsCoproduct]
 
 end OppositeProducts
 

Mathlib/Combinatorics/SimpleGraph/AdjMatrix.lean

@@ -243,14 +243,14 @@ theorem trace_adjMatrix [AddCommMonoid α] [One α] : Matrix.trace (G.adjMatrix
 variable {α}
 
 theorem adjMatrix_mul_self_apply_self [NonAssocSemiring α] (i : V) :
-    (G.adjMatrix α * G.adjMatrix α) i i = degree G i := by simp [degree]
+    (G.adjMatrix α * G.adjMatrix α) i i = degree G i := by simp
 #align simple_graph.adj_matrix_mul_self_apply_self SimpleGraph.adjMatrix_mul_self_apply_self
 
 variable {G}
 
 -- @[simp] -- Porting note: simp can prove this
 theorem adjMatrix_mulVec_const_apply [Semiring α] {a : α} {v : V} :
-    (G.adjMatrix α).mulVec (Function.const _ a) v = G.degree v * a := by simp [degree]
+    (G.adjMatrix α).mulVec (Function.const _ a) v = G.degree v * a := by simp
 #align simple_graph.adj_matrix_mul_vec_const_apply SimpleGraph.adjMatrix_mulVec_const_apply
 
 theorem adjMatrix_mulVec_const_apply_of_regular [Semiring α] {d : ℕ} {a : α}

Mathlib/Data/Vector/Snoc.lean

@@ -49,8 +49,7 @@ theorem reverse_snoc : reverse (xs.snoc x) = x ::ᵥ (reverse xs) := by
   cases xs
   simp only [reverse, snoc, cons, toList_mk]
   congr
-  simp [toList, (·++·), Vector.append, Append.append]
-  rfl
+  simp [toList, Vector.append, Append.append]
 
 theorem replicate_succ_to_snoc (val : α) :
     replicate (n+1) val = (replicate n val).snoc val := by

Mathlib/ModelTheory/Semantics.lean

@@ -182,7 +182,7 @@ theorem realize_varsToConstants [L[[α]].Structure M] [(lhomWithConstants L α).
   induction' t with ab n f ts ih
   · cases' ab with a b
     --Porting note: both cases were `simp [Language.con]`
-    · simp [Language.con, realize, constantMap, funMap_eq_coe_constants]
+    · simp [Language.con, realize, funMap_eq_coe_constants]
     · simp [realize, constantMap]
   · simp only [realize, constantsOn, mk₂_Functions, ih]
     --Porting note: below lemma does not work with simp for some reason

Mathlib/Testing/SlimCheck/Sampleable.lean

@@ -200,7 +200,7 @@ instance Nat.sampleableExt : SampleableExt Nat :=
 
 instance Fin.sampleableExt {n : Nat} : SampleableExt (Fin (n.succ)) :=
   mkSelfContained (do choose (Fin n.succ) (Fin.ofNat 0) (Fin.ofNat (← getSize)) (by
-    simp only [LE.le, Fin.ofNat, Nat.zero_mod, Fin.zero_eta, Fin.val_zero, Nat.le_eq]
+    simp only [LE.le, Fin.ofNat, Nat.zero_mod, Fin.zero_eta, Fin.val_zero]
     exact Nat.zero_le _))
 
 instance Int.sampleableExt : SampleableExt Int :=