suggestions from review

kim-em · kim-em · commit fc678697ddd8 · 2025-01-05T14:43:45.000+11:00
diff --git a/Mathlib/Algebra/Category/ModuleCat/Subobject.lean b/Mathlib/Algebra/Category/ModuleCat/Subobject.lean
@@ -85,7 +85,6 @@ theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap
   suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = x by
     convert this
   rw [Iso.trans_inv, ← LinearMap.coe_comp, ← hom_comp, Category.assoc]
-  simp only [Category.assoc, kernelSubobject_arrow', kernelIsoKer_inv_kernel_ι]
   simp
 
 /-- An extensionality lemma showing that two elements of a cokernel by an image
diff --git a/Mathlib/Data/Matrix/ColumnRowPartitioned.lean b/Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@@ -125,8 +125,7 @@ lemma fromRows_toRows (A : Matrix (m₁ ⊕ m₂) n R) : fromRows A.toRows₁ A.
 
 lemma fromRows_inj : Function.Injective2 (@fromRows R m₁ m₂ n) := by
   intros x1 x2 y1 y2
-  simp only [funext_iff, ← Matrix.ext_iff]
-  simp
+  simp [← Matrix.ext_iff]
 
 lemma fromCols_inj : Function.Injective2 (@fromCols R m n₁ n₂) := by
   intros x1 x2 y1 y2
diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
@@ -73,8 +73,7 @@ lemma isSemisimple_iff' :
 
 lemma isSemisimple_iff :
     f.IsSemisimple ↔ ∀ p ∈ invtSubmodule f, ∃ q ∈ invtSubmodule f, IsCompl p q := by
-  simp_rw [isSemisimple_iff']
-  simp
+  simp [isSemisimple_iff']
 
 lemma isSemisimple_restrict_iff (p) (hp : p ∈ invtSubmodule f) :
     IsSemisimple (LinearMap.restrict f hp) ↔
