Use using

adomani · adomani · commit 6cde5975789f · 2024-03-24T05:00:47.000Z
diff --git a/Mathlib/Algebra/Category/ModuleCat/Subobject.lean b/Mathlib/Algebra/Category/ModuleCat/Subobject.lean
@@ -45,9 +45,7 @@ noncomputable def subobjectModule : Subobject M ≃o Submodule R M :=
         · apply LinearEquiv.toModuleIso'Left
           apply LinearEquiv.ofBijective (LinearMap.codRestrict (LinearMap.range S.arrow) S.arrow _)
           constructor
-          · simp only [← LinearMap.ker_eq_bot, LinearMap.mem_range, exists_apply_eq_apply,
-            forall_const, LinearMap.ker_codRestrict]
-            rw [ker_eq_bot_of_mono]
+          · simpa [← LinearMap.ker_eq_bot, LinearMap.ker_codRestrict] using ker_eq_bot_of_mono ..
           · rw [← LinearMap.range_eq_top, LinearMap.range_codRestrict, Submodule.comap_subtype_self]
             exact LinearMap.mem_range_self _
         · apply LinearMap.ext
