chore: round 37 - remove unused simp args

Author: nomeata

Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean

@@ -616,9 +616,7 @@ instance biproduct.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p
   have : biproduct.map p =
       (biproduct.isoCoproduct _).hom ≫ Sigma.map p ≫ (biproduct.isoCoproduct _).inv := by
     ext
-    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc,
-      ι_colimMap_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc,
-        Cofan.mk_ι_app, ι_π, ι_π_assoc]
+    simp only [map_π, isoCoproduct_hom, isoCoproduct_inv, Category.assoc, ι_desc_assoc, ι_π_assoc]
     split
     · subst_vars
       simp

Mathlib/CategoryTheory/Limits/Shapes/SequentialProduct.lean

@@ -86,7 +86,7 @@ lemma functorMap_commSq_aux {n m k : ℕ} (h : n ≤ m) (hh : ¬(k < m)) :
     rw [this, op_comp, Functor.map_comp]
     slice_lhs 2 4 => rw [ih]
     simp only [ homOfLE_leOfHom, Functor.ofOpSequence_map_homOfLE_succ,
-      functorMap, dite_eq_ite, limMap_π_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app]
+      functorMap, dite_eq_ite]
     split_ifs
     · omega
     simp [dif_neg (by lia : ¬(k < m)), dif_neg hh]
@@ -149,14 +149,14 @@ set_option backward.isDefEq.respectTransparency false in
 lemma cone_π_app_comp_Pi_π_pos (m n : ℕ) (h : n < m) : (cone f).π.app ⟨m⟩ ≫
     Pi.π (fun i ↦ if _ : i < m then M i else N i) n =
     Pi.π _ n ≫ eqToHom (functorObj_eq_pos h).symm := by
-  simp [cone_π_app, limMap_π, Discrete.functor_obj_eq_as, Discrete.natTrans_app, dif_pos h]
+  simp [cone_π_app, dif_pos h]
 
 set_option backward.defeqAttrib.useBackward true in
 set_option backward.isDefEq.respectTransparency false in
 @[reassoc]
 lemma cone_π_app_comp_Pi_π_neg (m n : ℕ) (h : ¬(n < m)) : (cone f).π.app ⟨m⟩ ≫ Pi.π _ n =
     Pi.π _ n ≫ f n ≫ eqToHom (functorObj_eq_neg h).symm := by
-  simp [cone_π_app, limMap_π, Discrete.functor_obj_eq_as, Discrete.natTrans_app, dif_neg h]
+  simp [cone_π_app, dif_neg h]
 
 set_option backward.isDefEq.respectTransparency false in
 /--