diff --git a/Mathlib/Algebra/Category/GroupCat/Basic.lean b/Mathlib/Algebra/Category/GroupCat/Basic.lean
index 1ccfa9fa96f6e..1575df5c7f3fc 100644
--- a/Mathlib/Algebra/Category/GroupCat/Basic.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Basic.lean
@@ -363,9 +363,7 @@ set_option linter.uppercaseLean3 false in
 -- the forgetful functor is representable.
 theorem injective_of_mono {G H : AddCommGroupCat.{0}} (f : G ⟶ H) [Mono f] : Function.Injective f :=
   fun g₁ g₂ h => by
-  have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by
-    apply int_hom_ext
-    simpa using h
+  have t0 : asHom g₁ ≫ f = asHom g₂ ≫ f := by aesop_cat
   have t1 : asHom g₁ = asHom g₂ := (cancel_mono _).1 t0
   apply asHom_injective t1
 set_option linter.uppercaseLean3 false in
diff --git a/Mathlib/Algebra/Category/GroupCat/Colimits.lean b/Mathlib/Algebra/Category/GroupCat/Colimits.lean
index 519669381181c..8d175e70549a1 100644
--- a/Mathlib/Algebra/Category/GroupCat/Colimits.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Colimits.lean
@@ -327,7 +327,7 @@ noncomputable def cokernelIsoQuotient {G H : AddCommGroupCat.{u}} (f : G ⟶ H)
     simp only [coequalizer_as_cokernel, cokernel.π_desc_assoc, Category.comp_id]
     rfl
   inv_hom_id := by
-    ext x : 2
+    ext x
     exact QuotientAddGroup.induction_on x <| cokernel.π_desc_apply f _ _
 #align AddCommGroup.cokernel_iso_quotient AddCommGroupCat.cokernelIsoQuotient
 
diff --git a/Mathlib/Algebra/Category/GroupCat/Limits.lean b/Mathlib/Algebra/Category/GroupCat/Limits.lean
index c615bca17b0f5..4cb288bb46064 100644
--- a/Mathlib/Algebra/Category/GroupCat/Limits.lean
+++ b/Mathlib/Algebra/Category/GroupCat/Limits.lean
@@ -431,6 +431,8 @@ def kernelIsoKer {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
     rintro ⟨x, (hx : f _ = 0)⟩
     exact hx
   hom_inv_id := by
+    -- Porting note: it would be nice to do the next two steps by a single `ext`,
+    -- but this will require thinking carefully about the relative priorities of `@[ext]` lemmas.
     refine equalizer.hom_ext ?_
     ext x
     dsimp
diff --git a/Mathlib/Algebra/Homology/ImageToKernel.lean b/Mathlib/Algebra/Homology/ImageToKernel.lean
index f4034179fbe31..8af386b61545d 100644
--- a/Mathlib/Algebra/Homology/ImageToKernel.lean
+++ b/Mathlib/Algebra/Homology/ImageToKernel.lean
@@ -274,11 +274,8 @@ theorem imageSubobjectMap_comp_imageToKernel (p : α.right = β.left) :
 #align image_subobject_map_comp_image_to_kernel imageSubobjectMap_comp_imageToKernel
 
 variable [HasCokernel (imageToKernel f g w)] [HasCokernel (imageToKernel f' g' w')]
-
 variable [HasCokernel (imageToKernel f₁ g₁ w₁)]
-
 variable [HasCokernel (imageToKernel f₂ g₂ w₂)]
-
 variable [HasCokernel (imageToKernel f₃ g₃ w₃)]
 
 /-- Given compatible commutative squares between
@@ -286,10 +283,9 @@ a pair `f g` and a pair `f' g'` satisfying `f ≫ g = 0` and `f' ≫ g' = 0`,
 we get a morphism on homology.
 -/
 def homology.map (p : α.right = β.left) : homology f g w ⟶ homology f' g' w' :=
-  cokernel.desc _ (kernelSubobjectMap β ≫ cokernel.π _)
-    (by
-      rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
-      simp only [cokernel.condition, comp_zero])
+  cokernel.desc _ (kernelSubobjectMap β ≫ cokernel.π _) <| by
+    rw [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p]
+    simp only [cokernel.condition, comp_zero]
 #align homology.map homology.map
 
 -- porting note: removed elementwise attribute which does not seem to be helpful here,
@@ -318,13 +314,15 @@ theorem homology.map_desc (p : α.right = β.left) {D : V} (k : (kernelSubobject
     (z : imageToKernel f' g' w' ≫ k = 0) :
     homology.map w w' α β p ≫ homology.desc f' g' w' k z =
       homology.desc f g w (kernelSubobjectMap β ≫ k)
-        (by simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]) :=
-  by ext ; simp only [homology.π_desc, homology.π_map_assoc]
+        (by simp only [imageSubobjectMap_comp_imageToKernel_assoc w w' α β p, z, comp_zero]) := by
+  ext
+  simp only [homology.π_desc, homology.π_map_assoc]
 #align homology.map_desc homology.map_desc
 
 @[simp]
 theorem homology.map_id : homology.map w w (𝟙 _) (𝟙 _) rfl = 𝟙 _ := by
-  ext ; simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
+  ext
+  simp only [homology.π_map, kernelSubobjectMap_id, Category.id_comp, Category.comp_id]
 #align homology.map_id homology.map_id
 
 /-- Auxiliary lemma for homology computations. -/
@@ -340,7 +338,8 @@ theorem homology.comp_right_eq_comp_left {V : Type _} [Category V] {A₁ B₁ C
 theorem homology.map_comp (p₁ : α₁.right = β₁.left) (p₂ : α₂.right = β₂.left) :
     homology.map w₁ w₂ α₁ β₁ p₁ ≫ homology.map w₂ w₃ α₂ β₂ p₂ =
       homology.map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) (homology.comp_right_eq_comp_left p₁ p₂) := by
-  ext ; simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
+  ext
+  simp only [kernelSubobjectMap_comp, homology.π_map_assoc, homology.π_map, Category.assoc]
 #align homology.map_comp homology.map_comp
 
 /-- An isomorphism between two three-term complexes induces an isomorphism on homology. -/
@@ -414,17 +413,16 @@ this variant provides a morphism
 which is sometimes more convenient.
 -/
 def imageToKernel' (w : f ≫ g = 0) : image f ⟶ kernel g :=
-  kernel.lift g (image.ι f)
-    (by
-      ext
-      simpa using w)
+  kernel.lift g (image.ι f) <| by
+    ext
+    simpa using w
 #align image_to_kernel' imageToKernel'
 
 @[simp]
 theorem imageSubobjectIso_imageToKernel' (w : f ≫ g = 0) :
     (imageSubobjectIso f).hom ≫ imageToKernel' f g w =
       imageToKernel f g w ≫ (kernelSubobjectIso g).hom := by
-  apply equalizer.hom_ext
+  ext
   simp [imageToKernel']
 #align image_subobject_iso_image_to_kernel' imageSubobjectIso_imageToKernel'
 
@@ -447,12 +445,15 @@ def homologyIsoCokernelImageToKernel' (w : f ≫ g = 0) :
   inv := cokernel.map _ _ (imageSubobjectIso f).inv (kernelSubobjectIso g).inv
       (by simp only [imageToKernel'_kernelSubobjectIso])
   hom_inv_id := by
+    -- Just calling `ext` here uses the higher priority `homology.ext`,
+    -- which precomposes with `homology.π`.
+    -- As we are trying to work in terms of `cokernel`, it is better to use `coequalizer.hom_ext`.
     apply coequalizer.hom_ext
     simp only [Iso.hom_inv_id_assoc, cokernel.π_desc, cokernel.π_desc_assoc, Category.assoc,
       coequalizer_as_cokernel]
     exact (Category.comp_id _).symm
   inv_hom_id := by
-    apply coequalizer.hom_ext
+    ext
     simp only [Iso.inv_hom_id_assoc, cokernel.π_desc, Category.comp_id, cokernel.π_desc_assoc,
       Category.assoc]
 #align homology_iso_cokernel_image_to_kernel' homologyIsoCokernelImageToKernel'
@@ -464,7 +465,7 @@ variable [HasEqualizers V]
 def homologyIsoCokernelLift (w : f ≫ g = 0) : homology f g w ≅ cokernel (kernel.lift g f w) := by
   refine' homologyIsoCokernelImageToKernel' f g w ≪≫ _
   have p : factorThruImage f ≫ imageToKernel' f g w = kernel.lift g f w := by
-    apply equalizer.hom_ext
+    ext
     simp [imageToKernel']
   exact (cokernelEpiComp _ _).symm ≪≫ cokernelIsoOfEq p
 #align homology_iso_cokernel_lift homologyIsoCokernelLift
diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean
index 39eb6134e545b..8db04120ac982 100644
--- a/Mathlib/Algebra/Homology/Opposite.lean
+++ b/Mathlib/Algebra/Homology/Opposite.lean
@@ -71,9 +71,7 @@ def homologyOp {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
     homology g.op f.op (by rw [← op_comp, w, op_zero]) ≅ Opposite.op (homology f g w) :=
   cokernelIsoOfEq (imageToKernel_op _ _ w) ≪≫ cokernelEpiComp _ _ ≪≫ cokernelCompIsIso _ _ ≪≫
     cokernelOpOp _ ≪≫ (homologyIsoKernelDesc _ _ _ ≪≫
-    kernelIsoOfEq (by
-    -- Porting note: broken ext
-      apply coequalizer.hom_ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
+    kernelIsoOfEq (by ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
     kernelCompMono _ (image.ι g)).op
 #align homology_op homologyOp
 
@@ -83,9 +81,7 @@ def homologyUnop {X Y Z : Vᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0)
     homology g.unop f.unop (by rw [← unop_comp, w, unop_zero]) ≅ Opposite.unop (homology f g w) :=
   cokernelIsoOfEq (imageToKernel_unop _ _ w) ≪≫ cokernelEpiComp _ _ ≪≫ cokernelCompIsIso _ _ ≪≫
     cokernelUnopUnop _ ≪≫ (homologyIsoKernelDesc _ _ _ ≪≫
-    kernelIsoOfEq (by
-    -- Porting note: broken ext
-      apply coequalizer.hom_ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
+    kernelIsoOfEq (by ext; simp only [image.fac, cokernel.π_desc, cokernel.π_desc_assoc]) ≪≫
     kernelCompMono _ (image.ι g)).unop
 #align homology_unop homologyUnop
 
diff --git a/Mathlib/Algebra/Homology/QuasiIso.lean b/Mathlib/Algebra/Homology/QuasiIso.lean
index ac597e317cbd9..7118c5924d0ac 100644
--- a/Mathlib/Algebra/Homology/QuasiIso.lean
+++ b/Mathlib/Algebra/Homology/QuasiIso.lean
@@ -114,7 +114,7 @@ noncomputable def toSingle₀CokernelAtZeroIso : cokernel (X.d 1 0) ≅ Y :=
 theorem toSingle₀CokernelAtZeroIso_hom_eq [hf : QuasiIso f] :
     f.toSingle₀CokernelAtZeroIso.hom =
       cokernel.desc (X.d 1 0) (f.f 0) (by rw [← f.2 1 0 rfl]; exact comp_zero) := by
-  apply coequalizer.hom_ext
+  ext
   dsimp only [toSingle₀CokernelAtZeroIso, ChainComplex.homologyZeroIso, homologyOfZeroRight,
     homology.mapIso, ChainComplex.homologyFunctor0Single₀, cokernel.map]
   dsimp [asIso]
@@ -164,7 +164,7 @@ noncomputable def fromSingle₀KernelAtZeroIso [hf : QuasiIso f] : kernel (X.d 0
 theorem fromSingle₀KernelAtZeroIso_inv_eq [hf : QuasiIso f] :
     f.fromSingle₀KernelAtZeroIso.inv =
       kernel.lift (X.d 0 1) (f.f 0) (by rw [f.2 0 1 rfl]; exact zero_comp) := by
-  apply equalizer.hom_ext
+  ext
   dsimp only [fromSingle₀KernelAtZeroIso, CochainComplex.homologyZeroIso, homologyOfZeroLeft,
     homology.mapIso, CochainComplex.homologyFunctor0Single₀, kernel.map]
   simp only [Iso.trans_inv, Iso.app_inv, Iso.symm_inv, Category.assoc, equalizer_as_kernel,
diff --git a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
index b968ddadc06dc..fa2f0039bedd6 100644
--- a/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
+++ b/Mathlib/AlgebraicGeometry/PresheafedSpace.lean
@@ -186,6 +186,10 @@ instance categoryOfPresheafedSpaces : Category (PresheafedSpace C) where
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.category_of_PresheafedSpaces AlgebraicGeometry.PresheafedSpace.categoryOfPresheafedSpaces
 
+variable {C}
+
+-- Porting note: adding an ext lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 theorem ext {X Y : PresheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
     (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
diff --git a/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean b/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean
index e5a3072fe9fa6..6803743f3ffdc 100644
--- a/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean
+++ b/Mathlib/AlgebraicGeometry/PresheafedSpace/HasColimits.lean
@@ -167,8 +167,8 @@ def pushforwardDiagramToColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
       (op ((Opens.map (F.map g).base).obj ((Opens.map (colimit.ι (F ⋙ forget C) j₃)).obj U.unop)))
       (op ((Opens.map (colimit.ι (F ⋙ PresheafedSpace.forget C) j₂)).obj (unop U)))
       _]
-    -- Now we show the open sets are equal.
     swap
+    -- Now we show the open sets are equal.
     · apply unop_injective
       rw [← Opens.map_comp_obj]
       congr
@@ -212,11 +212,12 @@ def colimitCocone (F : J ⥤ PresheafedSpace.{_, _, v} C) : Cocone F where
         { base := colimit.ι (F ⋙ PresheafedSpace.forget C) j
           c := limit.π _ (op j) }
       naturality := fun {j j'} f => by
-        fapply PresheafedSpace.ext
+        ext1
+        -- See https://github.com/leanprover/std4/pull/158
+        swap
         · ext x
           exact colimit.w_apply (F ⋙ PresheafedSpace.forget C) f x
-        · ext U
-          rcases U with ⟨U, hU⟩
+        · ext ⟨U, hU⟩
           dsimp
           rw [PresheafedSpace.id_c_app, map_id]
           erw [id_comp]
@@ -303,11 +304,12 @@ set_option linter.uppercaseLean3 false in
 
 theorem desc_fac (F : J ⥤ PresheafedSpace.{_, _, v} C) (s : Cocone F) (j : J) :
     (colimitCocone F).ι.app j ≫ desc F s = s.ι.app j := by
-  fapply PresheafedSpace.ext
+  ext U
+  -- See https://github.com/leanprover/std4/pull/158
+  swap
   · simp [desc]
   · -- Porting note : the original proof is just `ext; dsimp [desc, descCApp]; simpa`,
     -- but this has to be expanded a bit
-    ext U
     rw [NatTrans.comp_app, PresheafedSpace.comp_c_app, whiskerRight_app]
     dsimp [desc, descCApp]
     simp only [eqToHom_app, op_obj, Opens.map_comp_obj, eqToHom_map, Functor.leftOp, assoc]
@@ -331,14 +333,14 @@ def colimitCoconeIsColimit (F : J ⥤ PresheafedSpace.{_, _, v} C) :
     have t :
       m.base =
         colimit.desc (F ⋙ PresheafedSpace.forget C) ((PresheafedSpace.forget C).mapCocone s) := by
-      apply CategoryTheory.Limits.colimit.hom_ext
-      intro j
-      apply ContinuousMap.ext
-      intro x
+      dsimp
+      ext j
       rw [colimit.ι_desc, mapCocone_ι_app, ← w j]
       simp
-    fapply PresheafedSpace.ext
+    ext : 1
+    swap
     -- could `ext` please not reorder goals?
+    -- See https://github.com/leanprover/std4/pull/158
     · exact t
     · refine NatTrans.ext _ _ (funext fun U => limit_obj_ext fun j => ?_)
       dsimp only [colimitCocone_pt, colimit_carrier, leftOp_obj, pushforwardDiagramToColimit_obj,
diff --git a/Mathlib/AlgebraicGeometry/SheafedSpace.lean b/Mathlib/AlgebraicGeometry/SheafedSpace.lean
index 2d928a28f2b8d..6bb3083ad7f81 100644
--- a/Mathlib/AlgebraicGeometry/SheafedSpace.lean
+++ b/Mathlib/AlgebraicGeometry/SheafedSpace.lean
@@ -90,6 +90,13 @@ instance : Category (SheafedSpace C) :=
   show Category (InducedCategory (PresheafedSpace C) SheafedSpace.toPresheafedSpace) by
     infer_instance
 
+-- Porting note: adding an ext lemma.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
+@[ext]
+theorem ext {X Y : SheafedSpace C} (α β : X ⟶ Y) (w : α.base = β.base)
+    (h : α.c ≫ whiskerRight (eqToHom (by rw [w])) _ = β.c) : α = β :=
+  PresheafedSpace.ext α β w h
+
 /-- Forgetting the sheaf condition is a functor from `SheafedSpace C` to `PresheafedSpace C`. -/
 def forgetToPresheafedSpace : SheafedSpace C ⥤ PresheafedSpace C :=
   inducedFunctor _
diff --git a/Mathlib/AlgebraicGeometry/Spec.lean b/Mathlib/AlgebraicGeometry/Spec.lean
index b14a2bd435a70..3cd4e6c573db2 100644
--- a/Mathlib/AlgebraicGeometry/Spec.lean
+++ b/Mathlib/AlgebraicGeometry/Spec.lean
@@ -189,13 +189,16 @@ theorem Spec.basicOpen_hom_ext {X : RingedSpace.{u}} {R : CommRingCat.{u}}
       (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) =
         toOpen R U ≫ β.c.app (op U)) :
     α = β := by
-  refine PresheafedSpace.ext (α := α) (β := β) w ?_
+  ext : 1
+  -- See https://github.com/leanprover/std4/pull/158
+  swap
+  · exact w
   · apply
       ((TopCat.Sheaf.pushforward β.base).obj X.sheaf).hom_ext _ PrimeSpectrum.isBasis_basic_opens
     intro r
     apply (StructureSheaf.to_basicOpen_epi R r).1
-    specialize h r
     -- Porting note : was a one-liner `simpa using h r`
+    specialize h r
     simp only [sheafedSpaceObj_carrier, Functor.op_obj, unop_op, TopCat.Presheaf.pushforwardObj_obj,
       sheafedSpaceObj_presheaf, Category.assoc] at h
     rw [NatTrans.comp_app, ←h]
diff --git a/Mathlib/AlgebraicGeometry/Stalks.lean b/Mathlib/AlgebraicGeometry/Stalks.lean
index c52b31f498e26..9119eee54222e 100644
--- a/Mathlib/AlgebraicGeometry/Stalks.lean
+++ b/Mathlib/AlgebraicGeometry/Stalks.lean
@@ -104,6 +104,7 @@ set_option linter.uppercaseLean3 false in
 theorem restrictStalkIso_inv_eq_ofRestrict {U : TopCat} (X : PresheafedSpace.{_, _, v} C)
     {f : U ⟶ (X : TopCat.{v})} (h : OpenEmbedding f) (x : U) :
     (X.restrictStalkIso h x).inv = stalkMap (X.ofRestrict h) x := by
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun V => ?_
   induction V with | h V => ?_
   let i : (h.isOpenMap.functorNhds x).obj ((OpenNhds.map f x).obj V) ⟶ V :=
@@ -147,6 +148,7 @@ theorem comp {X Y Z : PresheafedSpace.{_, _, v} C} (α : X ⟶ Y) (β : Y ⟶ Z)
       (stalkMap β (α.base x) : Z.stalk (β.base (α.base x)) ⟶ Y.stalk (α.base x)) ≫
         (stalkMap α x : Y.stalk (α.base x) ⟶ X.stalk x) := by
   dsimp [stalkMap, stalkFunctor, stalkPushforward]
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun U => ?_
   induction U with | h U => ?_
   cases U
@@ -165,8 +167,10 @@ either side of the equality.
 theorem congr {X Y : PresheafedSpace.{_, _, v} C} (α β : X ⟶ Y)
     (h₁ : α = β) (x x' : X) (h₂ : x = x') :
     stalkMap α x ≫ eqToHom (show X.stalk x = X.stalk x' by rw [h₂]) =
-      eqToHom (show Y.stalk (α.base x) = Y.stalk (β.base x') by rw [h₁, h₂]) ≫ stalkMap β x' :=
-  stalk_hom_ext _ fun U hx => by subst h₁; subst h₂; simp
+      eqToHom (show Y.stalk (α.base x) = Y.stalk (β.base x') by rw [h₁, h₂]) ≫ stalkMap β x' := by
+  ext
+  substs h₁ h₂
+  simp
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.PresheafedSpace.stalk_map.congr AlgebraicGeometry.PresheafedSpace.stalkMap.congr
 
@@ -225,6 +229,7 @@ theorem stalkSpecializes_stalkMap {X Y : PresheafedSpace.{_, _, v} C}
   -- Porting note : the original one liner `dsimp [stalkMap]; simp [stalkMap]` doesn't work,
   -- I had to uglify this
   dsimp [stalkSpecializes, stalkMap, stalkFunctor, stalkPushforward]
+  -- We can't use `ext` here due to https://github.com/leanprover/std4/pull/159
   refine colimit.hom_ext fun j => ?_
   induction j with | h j => ?_
   dsimp
diff --git a/Mathlib/AlgebraicGeometry/StructureSheaf.lean b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
index f7ae2e46e1385..41e3fdd65ab32 100644
--- a/Mathlib/AlgebraicGeometry/StructureSheaf.lean
+++ b/Mathlib/AlgebraicGeometry/StructureSheaf.lean
@@ -577,6 +577,10 @@ def stalkIso (x : PrimeSpectrum.Top R) :
   hom := stalkToFiberRingHom R x
   inv := localizationToStalk R x
   hom_inv_id :=
+    -- Porting note: We should be able to replace the next two lines with `ext U hxU s`,
+    -- but there seems to be a bug in `ext` whereby
+    -- it will not do multiple introductions for a single lemma, if you name the arguments.
+    -- See https://github.com/leanprover/std4/pull/159
     (structureSheaf R).presheaf.stalk_hom_ext fun U hxU => by
       ext s
       simp only [FunctorToTypes.map_comp_apply, CommRingCat.forget_map,
diff --git a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
index 03496bc795805..d942d7f08de02 100644
--- a/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
+++ b/Mathlib/AlgebraicTopology/SplitSimplicialObject.lean
@@ -215,9 +215,7 @@ def summand (A : IndexSet Δ) : C :=
 variable [HasFiniteCoproducts C]
 
 /-- The coproduct of the family `summand N Δ` -/
-@[simp]
-def coprod :=
-  ∐ summand N Δ
+abbrev coprod := ∐ summand N Δ
 #align simplicial_object.splitting.coprod SimplicialObject.Splitting.coprod
 
 variable {Δ}
@@ -301,8 +299,7 @@ theorem ιSummand_comp_app (f : X ⟶ Y) {Δ : SimplexCategoryᵒᵖ} (A : Index
 theorem hom_ext' {Z : C} {Δ : SimplexCategoryᵒᵖ} (f g : X.obj Δ ⟶ Z)
     (h : ∀ A : IndexSet Δ, s.ιSummand A ≫ f = s.ιSummand A ≫ g) : f = g := by
   rw [← cancel_epi (s.iso Δ).hom]
-  apply colimit.hom_ext
-  rintro ⟨A⟩
+  ext A
   simpa only [ιSummand_eq, iso_hom, map, colimit.ι_desc_assoc, Cofan.mk_ι_app] using h A
 #align simplicial_object.splitting.hom_ext' SimplicialObject.Splitting.hom_ext'
 
@@ -338,7 +335,7 @@ def ofIso (e : X ≅ Y) : Splitting Y where
   ι n := s.ι n ≫ e.hom.app (op [n])
   map_isIso Δ := by
     convert (inferInstance : IsIso ((s.iso Δ).hom ≫ e.hom.app Δ))
-    apply colimit.hom_ext
+    ext
     simp [map]
 #align simplicial_object.splitting.of_iso SimplicialObject.Splitting.ofIso
 
diff --git a/Mathlib/CategoryTheory/Abelian/Basic.lean b/Mathlib/CategoryTheory/Abelian/Basic.lean
index 0ade7bfd48cb6..da348bef95d96 100644
--- a/Mathlib/CategoryTheory/Abelian/Basic.lean
+++ b/Mathlib/CategoryTheory/Abelian/Basic.lean
@@ -26,7 +26,7 @@ and if every monomorphism and epimorphism is normal.
 
 It should be noted that if we also assume coproducts, then preadditivity is
 actually a consequence of the other properties, as we show in
-`non_preadditive_abelian.lean`. However, this fact is of little practical
+`NonPreadditiveAbelian.lean`. However, this fact is of little practical
 relevance, since essentially all interesting abelian categories come with a
 preadditive structure. In this way, by requiring preadditivity, we allow the
 user to pass in the "native" preadditive structure for the specific category they are
@@ -34,7 +34,7 @@ working with.
 
 ## Main definitions
 
-* `Abelian` is the type class indicating that a category is abelian. It extends `preadditive`.
+* `Abelian` is the type class indicating that a category is abelian. It extends `Preadditive`.
 * `Abelian.image f` is `kernel (cokernel.π f)`, and
 * `Abelian.coimage f` is `cokernel (kernel.ι f)`.
 
@@ -42,7 +42,7 @@ working with.
 
 * In an abelian category, mono + epi = iso.
 * If `f : X ⟶ Y`, then the map `factorThruImage f : X ⟶ image f` is an epimorphism, and the map
-  `factor_thru_coimage f : coimage f ⟶ Y` is a monomorphism.
+  `factorThruCoimage f : coimage f ⟶ Y` is a monomorphism.
 * Factoring through the image and coimage is a strong epi-mono factorisation. This means that
   * every abelian category has images. We provide the isomorphism
     `imageIsoImage : abelian.image f ≅ limits.image f`.
@@ -74,7 +74,7 @@ convention:
 * If the statement of a theorem involves limits, the existence of these limits should be made an
   explicit typeclass parameter.
 * If a limit only appears in a proof, but not in the statement of a theorem, the limit should not
-  be a typeclass parameter, but instead be created using `abelian.has_pullbacks` or a similar
+  be a typeclass parameter, but instead be created using `Abelian.hasPullbacks` or a similar
   definition.
 
 ## References
@@ -150,7 +150,8 @@ def imageMonoFactorisation {X Y : C} (f : X ⟶ Y) : MonoFactorisation f where
 
 theorem imageMonoFactorisation_e' {X Y : C} (f : X ⟶ Y) :
     (imageMonoFactorisation f).e = cokernel.π _ ≫ Abelian.coimageImageComparison f := by
-  apply equalizer.hom_ext
+  dsimp
+  ext
   simp only [Abelian.coimageImageComparison, imageMonoFactorisation_e, Category.assoc,
     cokernel.π_desc_assoc]
 #align category_theory.abelian.of_coimage_image_comparison_is_iso.image_mono_factorisation_e' CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageMonoFactorisation_e'
@@ -166,7 +167,7 @@ def imageFactorisation {X Y : C} (f : X ⟶ Y) [IsIso (Abelian.coimageImageCompa
         rw [imageMonoFactorisation_m]
         simp only [Category.assoc]
         rw [IsIso.inv_comp_eq]
-        apply coequalizer.hom_ext
+        ext
         simp }
 #align category_theory.abelian.of_coimage_image_comparison_is_iso.image_factorisation CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.imageFactorisation
 
@@ -401,7 +402,7 @@ instance : IsIso (coimageImageComparison f) := by
     IsIso.of_iso
       (IsImage.isoExt (coimageStrongEpiMonoFactorisation f).toMonoIsImage
         (imageStrongEpiMonoFactorisation f).toMonoIsImage)
-  apply coequalizer.hom_ext; apply equalizer.hom_ext
+  ext
   change _ = _ ≫ (imageStrongEpiMonoFactorisation f).m
   simp [-imageStrongEpiMonoFactorisation_m]
 
@@ -420,7 +421,7 @@ abbrev coimageIsoImage' : Abelian.coimage f ≅ image f :=
 theorem coimageIsoImage'_hom :
     (coimageIsoImage' f).hom =
       cokernel.desc _ (factorThruImage f) (by simp [← cancel_mono (Limits.image.ι f)]) := by
-  apply coequalizer.hom_ext
+  ext
   simp only [← cancel_mono (Limits.image.ι f), IsImage.isoExt_hom, cokernel.π_desc,
     Category.assoc, IsImage.lift_ι, coimageStrongEpiMonoFactorisation_m,
     Limits.image.fac]
@@ -445,7 +446,7 @@ theorem imageIsoImage_hom_comp_image_ι : (imageIsoImage f).hom ≫ Limits.image
 theorem imageIsoImage_inv :
     (imageIsoImage f).inv =
       kernel.lift _ (Limits.image.ι f) (by simp [← cancel_epi (factorThruImage f)]) := by
-  apply image.ext; apply equalizer.hom_ext
+  ext
   rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
     imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
     kernel.lift_ι, Limits.image.fac]
diff --git a/Mathlib/CategoryTheory/Abelian/Exact.lean b/Mathlib/CategoryTheory/Abelian/Exact.lean
index 9a1bc1b36eddb..b0508718e3136 100644
--- a/Mathlib/CategoryTheory/Abelian/Exact.lean
+++ b/Mathlib/CategoryTheory/Abelian/Exact.lean
@@ -152,7 +152,7 @@ def isColimitCoimage (h : Exact f g) :
       (by rw [← cokernel.π_desc f u hu, ← Category.assoc, h.2, zero_comp]))
     (by aesop_cat) _
   intros _ _ _ _ hm
-  apply coequalizer.hom_ext
+  ext
   rw [hm, cokernel.π_desc]
 #align category_theory.abelian.is_colimit_coimage CategoryTheory.Abelian.isColimitCoimage
 
diff --git a/Mathlib/CategoryTheory/Abelian/FunctorCategory.lean b/Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
index 483bea7214de5..f3045b202c8a0 100644
--- a/Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
+++ b/Mathlib/CategoryTheory/Abelian/FunctorCategory.lean
@@ -68,8 +68,7 @@ def imageObjIso : (Abelian.image α).obj X ≅ Abelian.image (α.app X) :=
 theorem coimageImageComparison_app :
     coimageImageComparison (α.app X) =
       (coimageObjIso α X).inv ≫ (coimageImageComparison α).app X ≫ (imageObjIso α X).hom := by
-  apply coequalizer.hom_ext
-  apply equalizer.hom_ext
+  ext
   dsimp
   dsimp [imageObjIso, coimageObjIso, cokernel.map]
   simp only [coimage_image_factorisation, PreservesKernel.iso_hom, Category.assoc,
diff --git a/Mathlib/CategoryTheory/Abelian/Homology.lean b/Mathlib/CategoryTheory/Abelian/Homology.lean
index 2132802337146..0ea68e8d418ad 100644
--- a/Mathlib/CategoryTheory/Abelian/Homology.lean
+++ b/Mathlib/CategoryTheory/Abelian/Homology.lean
@@ -61,10 +61,7 @@ abbrev homologyK : A :=
   This is an isomorphism, and it is used in obtaining the API for `homology f g w`
   in the bottom of this file. -/
 abbrev homologyCToK : homologyC f g w ⟶ homologyK f g w :=
-  cokernel.desc _ (kernel.lift _ (kernel.ι _ ≫ cokernel.π _) (by simp))
-    (by
-      apply Limits.equalizer.hom_ext
-      simp)
+  cokernel.desc _ (kernel.lift _ (kernel.ι _ ≫ cokernel.π _) (by simp)) (by ext; simp)
 #align category_theory.abelian.homology_c_to_k CategoryTheory.Abelian.homologyCToK
 
 attribute [local instance] Pseudoelement.homToFun Pseudoelement.hasZero
@@ -223,7 +220,7 @@ theorem π'_map (α β h) : π' _ _ _ ≫ map w w' α β h =
     (kernelSubobjectIso g).inv ≫ kernelSubobjectMap β =
       kernel.map _ _ β.left β.right β.w.symm ≫ (kernelSubobjectIso _).inv := by
     rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv]
-    refine Limits.equalizer.hom_ext ?_
+    ext
     dsimp
     simp
   rw [this]
@@ -252,8 +249,7 @@ theorem map_eq_desc'_lift_left (α β h) :
   dsimp [π', lift]
   rw [Iso.eq_comp_inv]
   dsimp [homologyIsoKernelDesc]
-  -- Porting note: previously ext
-  apply Limits.equalizer.hom_ext
+  ext
   simp [h]
 #align homology.map_eq_desc'_lift_left homology.map_eq_desc'_lift_left
 
diff --git a/Mathlib/CategoryTheory/Abelian/Images.lean b/Mathlib/CategoryTheory/Abelian/Images.lean
index 352d088db4a42..1a1f2b8ad7062 100644
--- a/Mathlib/CategoryTheory/Abelian/Images.lean
+++ b/Mathlib/CategoryTheory/Abelian/Images.lean
@@ -107,20 +107,18 @@ in which this is always an isomorphism, is abelian.
 See <https://stacks.math.columbia.edu/tag/0107>
 -/
 def coimageImageComparison : Abelian.coimage f ⟶ Abelian.image f :=
-  cokernel.desc (kernel.ι f) (kernel.lift (cokernel.π f) f (by simp)) <|
-    by apply equalizer.hom_ext; simp
+  cokernel.desc (kernel.ι f) (kernel.lift (cokernel.π f) f (by simp)) (by ext; simp)
 #align category_theory.abelian.coimage_image_comparison CategoryTheory.Abelian.coimageImageComparison
 
 /-- An alternative formulation of the canonical map from the abelian coimage to the abelian image.
 -/
 def coimageImageComparison' : Abelian.coimage f ⟶ Abelian.image f :=
-  kernel.lift (cokernel.π f) (cokernel.desc (kernel.ι f) f (by simp))
-    (by apply coequalizer.hom_ext; simp)
+  kernel.lift (cokernel.π f) (cokernel.desc (kernel.ι f) f (by simp)) (by ext; simp)
 #align category_theory.abelian.coimage_image_comparison' CategoryTheory.Abelian.coimageImageComparison'
 
 theorem coimageImageComparison_eq_coimageImageComparison' :
     coimageImageComparison f = coimageImageComparison' f := by
-  apply coequalizer.hom_ext; apply equalizer.hom_ext
+  ext
   simp [coimageImageComparison, coimageImageComparison']
 #align category_theory.abelian.coimage_image_comparison_eq_coimage_image_comparison' CategoryTheory.Abelian.coimageImageComparison_eq_coimageImageComparison'
 
@@ -130,4 +128,3 @@ theorem coimage_image_factorisation : coimage.π f ≫ coimageImageComparison f
 #align category_theory.abelian.coimage_image_factorisation CategoryTheory.Abelian.coimage_image_factorisation
 
 end CategoryTheory.Abelian
-
diff --git a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
index 03d9720c928a3..a419283fffad2 100644
--- a/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
+++ b/Mathlib/CategoryTheory/Abelian/LeftDerived.lean
@@ -90,8 +90,8 @@ def leftDerivedZeroToSelfAppInv [EnoughProjectives C] [PreservesFiniteColimits F
     (asIso (cokernel.desc _ _ (exact_of_map_projectiveResolution F P).w)).inv ≫
       _ ≫ (homologyIsoCokernelLift _ _ _).inv ≫ (leftDerivedObjIso F 0 P).inv
   refine' cokernel.map _ _ (𝟙 _) (kernel.lift _ (𝟙 _) (by simp)) _
-  -- Porting note: this used to be ext ; simp
-  apply equalizer.hom_ext
+  ext
+  -- Porting note: this used to just be `simp`
   simp only [Category.assoc, kernel.lift_ι, Category.comp_id, Category.id_comp]
 #align category_theory.abelian.functor.left_derived_zero_to_self_app_inv CategoryTheory.Abelian.Functor.leftDerivedZeroToSelfAppInv
 
@@ -117,7 +117,7 @@ theorem leftDerivedZeroToSelfApp_comp_inv [EnoughProjectives C] [PreservesFinite
   -- Porting note: restructured proof to avoid `convert`
   conv_rhs => rw [← Category.id_comp (cokernel.π _)]
   congr
-  apply equalizer.hom_ext
+  ext
   -- Porting note: working around 'motive is not type correct'
   simp only [Category.id_comp]
   rw [Category.assoc, equalizer_as_kernel, kernel.lift_ι]
@@ -145,7 +145,7 @@ theorem leftDerivedZeroToSelfAppInv_comp [EnoughProjectives C] [PreservesFiniteC
   rw [IsIso.inv_comp_eq]
   -- Porting note: working around 'motive is not type correct'
   simp only [Category.comp_id]
-  apply coequalizer.hom_ext
+  ext
   simp only [cokernel.π_desc_assoc, Category.assoc, cokernel.π_desc, homology.desc']
   rw [← Category.assoc, ← Category.assoc (homologyIsoCokernelLift _ _ _).inv, Iso.inv_hom_id]
   simp only [Category.assoc, cokernel.π_desc, kernel.lift_ι_assoc, Category.id_comp]
diff --git a/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean b/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
index c9d1005b25706..6987a57f8a550 100644
--- a/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
+++ b/Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
@@ -366,7 +366,7 @@ theorem sub_self {X Y : C} (a : X ⟶ Y) : a - a = 0 := by
 theorem lift_sub_lift {X Y : C} (a b c d : X ⟶ Y) :
     prod.lift a b - prod.lift c d = prod.lift (a - c) (b - d) := by
   simp only [sub_def]
-  apply prod.hom_ext
+  ext
   · rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_fst, prod.lift_fst, prod.lift_fst]
   · rw [Category.assoc, σ_comp, prod.lift_map_assoc, prod.lift_snd, prod.lift_snd, prod.lift_snd]
 #align category_theory.non_preadditive_abelian.lift_sub_lift CategoryTheory.NonPreadditiveAbelian.lift_sub_lift
diff --git a/Mathlib/CategoryTheory/Abelian/Opposite.lean b/Mathlib/CategoryTheory/Abelian/Opposite.lean
index 772265ef61aa5..2bcfede424e82 100644
--- a/Mathlib/CategoryTheory/Abelian/Opposite.lean
+++ b/Mathlib/CategoryTheory/Abelian/Opposite.lean
@@ -56,12 +56,10 @@ def kernelOpUnop : (kernel f.op).unop ≅ cokernel f where
   hom_inv_id := by
     rw [← unop_id, ← (cokernel.desc f _ _).unop_op, ← unop_comp]
     congr 1
-    dsimp
-    apply equalizer.hom_ext
+    ext
     simp [← op_comp]
   inv_hom_id := by
-    dsimp
-    apply coequalizer.hom_ext
+    ext
     simp [← unop_comp]
 #align category_theory.kernel_op_unop CategoryTheory.kernelOpUnop
 
@@ -78,12 +76,10 @@ def cokernelOpUnop : (cokernel f.op).unop ≅ kernel f where
   hom_inv_id := by
     rw [← unop_id, ← (kernel.lift f _ _).unop_op, ← unop_comp]
     congr 1
-    dsimp
-    apply coequalizer.hom_ext
+    ext
     simp [← op_comp]
   inv_hom_id := by
-    dsimp
-    apply equalizer.hom_ext
+    ext
     simp [← unop_comp]
 #align category_theory.cokernel_op_unop CategoryTheory.cokernelOpUnop
 
diff --git a/Mathlib/CategoryTheory/Abelian/RightDerived.lean b/Mathlib/CategoryTheory/Abelian/RightDerived.lean
index de4ba103bd67c..6b9d82ed3f102 100644
--- a/Mathlib/CategoryTheory/Abelian/RightDerived.lean
+++ b/Mathlib/CategoryTheory/Abelian/RightDerived.lean
@@ -218,11 +218,11 @@ def rightDerivedZeroToSelfApp [EnoughInjectives C] [PreservesFiniteLimits F] {X
       (cokernel.desc _ (𝟙 _) (by simp)) (𝟙 _)
           (by
             -- Porting note: was ext; simp
-            apply coequalizer.hom_ext
+            ext
             dsimp
             simp) ≫
         -- Porting note: isIso_kernel_lift_of_exact_of_mono is no longer allowed as an
-        -- instance for reasons am I not privy to
+        -- instance for reasons I am not privy to
         have : IsIso <| kernel.lift _ _ (exact_of_map_injectiveResolution F P).w :=
           isIso_kernel_lift_of_exact_of_mono _ _ (exact_of_map_injectiveResolution F P)
         (asIso (kernel.lift _ _ (exact_of_map_injectiveResolution F P).w)).inv
@@ -274,8 +274,7 @@ theorem rightDerivedZeroToSelfAppInv_comp [EnoughInjectives C] [PreservesFiniteL
   -- Porting note: this IsIso instance used to be filled automatically
   apply (@IsIso.comp_inv_eq D _ _ _ _ _ ?_ _ _).mpr
   · rw [Category.id_comp]
-    -- Porting note: broken ext
-    apply equalizer.hom_ext
+    ext
     simp only [Limits.kernel.lift_ι_assoc,
       Category.assoc, Limits.kernel.lift_ι, homology.lift]
     rw [← Category.assoc, ← Category.assoc,
diff --git a/Mathlib/CategoryTheory/Adjunction/Comma.lean b/Mathlib/CategoryTheory/Adjunction/Comma.lean
index 5aaf963f8db48..53641b84a40b0 100644
--- a/Mathlib/CategoryTheory/Adjunction/Comma.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Comma.lean
@@ -52,9 +52,7 @@ def leftAdjointOfStructuredArrowInitialsAux (A : C) (B : D) :
   left_inv g := by
     let B' : StructuredArrow A G := StructuredArrow.mk ((⊥_ StructuredArrow A G).hom ≫ G.map g)
     let g' : ⊥_ StructuredArrow A G ⟶ B' := StructuredArrow.homMk g rfl
-    have : initial.to _ = g' := by
-      apply colimit.hom_ext
-      rintro ⟨⟨⟩⟩
+    have : initial.to _ = g' := by aesop_cat
     change CommaMorphism.right (initial.to B') = _
     rw [this]
     rfl
@@ -106,9 +104,7 @@ def rightAdjointOfCostructuredArrowTerminalsAux (B : D) (A : C) :
     let B' : CostructuredArrow G A :=
       CostructuredArrow.mk (G.map g ≫ (⊤_ CostructuredArrow G A).hom)
     let g' : B' ⟶ ⊤_ CostructuredArrow G A := CostructuredArrow.homMk g rfl
-    have : terminal.from _ = g' := by
-      apply limit.hom_ext
-      rintro ⟨⟨⟩⟩
+    have : terminal.from _ = g' := by aesop_cat
     change CommaMorphism.left (terminal.from B') = _
     rw [this]
     rfl
diff --git a/Mathlib/CategoryTheory/Closed/Cartesian.lean b/Mathlib/CategoryTheory/Closed/Cartesian.lean
index 8a3e61cbd1836..029f407f9f32a 100644
--- a/Mathlib/CategoryTheory/Closed/Cartesian.lean
+++ b/Mathlib/CategoryTheory/Closed/Cartesian.lean
@@ -354,12 +354,12 @@ def prodCoprodDistrib [HasBinaryCoproducts C] [CartesianClosed C] (X Y Z : C) :
     CartesianClosed.uncurry
       (coprod.desc (CartesianClosed.curry coprod.inl) (CartesianClosed.curry coprod.inr))
   hom_inv_id := by
-    apply coprod.hom_ext
+    ext
     rw [coprod.inl_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inl_desc, uncurry_curry]
     rw [coprod.inr_desc_assoc, comp_id, ← uncurry_natural_left, coprod.inr_desc, uncurry_curry]
   inv_hom_id := by
     rw [← uncurry_natural_right, ← eq_curry_iff]
-    apply coprod.hom_ext
+    ext
     rw [coprod.inl_desc_assoc, ← curry_natural_right, coprod.inl_desc, ← curry_natural_left,
       comp_id]
     rw [coprod.inr_desc_assoc, ← curry_natural_right, coprod.inr_desc, ← curry_natural_left,
diff --git a/Mathlib/CategoryTheory/Closed/Functor.lean b/Mathlib/CategoryTheory/Closed/Functor.lean
index 42756d994ea70..722a13ef41812 100644
--- a/Mathlib/CategoryTheory/Closed/Functor.lean
+++ b/Mathlib/CategoryTheory/Closed/Functor.lean
@@ -149,7 +149,7 @@ theorem frobeniusMorphism_mate (h : L ⊣ F) (A : C) :
   -- https://github.com/leanprover-community/mathlib4/issues/5164
   erw [exp.ev_coev]
   rw [F.map_id (A ⨯ L.obj B), comp_id]
-  apply prod.hom_ext
+  ext
   · rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_fst]
     simp
   · rw [assoc, assoc, ← h.counit_naturality, ← L.map_comp_assoc, assoc, inv_prodComparison_map_snd]
diff --git a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
index 51bcc2e0e5936..80478de3de955 100644
--- a/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
+++ b/Mathlib/CategoryTheory/ConcreteCategory/Basic.lean
@@ -107,7 +107,7 @@ def ConcreteCategory.funLike {X Y : C} : FunLike (X ⟶ Y) X (fun _ => Y) where
 attribute [local instance] ConcreteCategory.funLike
 
 /-- In any concrete category, we can test equality of morphisms by pointwise evaluations.-/
-@[ext 900] -- Porting note: lowered priority
+@[ext low] -- Porting note: lowered priority
 theorem ConcreteCategory.hom_ext {X Y : C} (f g : X ⟶ Y) (w : ∀ x : X, f x = g x) : f = g := by
   apply @Faithful.map_injective C _ (Type w) _ (forget C) _ X Y
   dsimp [forget]
diff --git a/Mathlib/CategoryTheory/Functor/Flat.lean b/Mathlib/CategoryTheory/Functor/Flat.lean
index 01ea554edb789..af1cc296bb939 100644
--- a/Mathlib/CategoryTheory/Functor/Flat.lean
+++ b/Mathlib/CategoryTheory/Functor/Flat.lean
@@ -364,6 +364,9 @@ noncomputable def lanEvaluationIsoColim (F : C ⥤ D) (X : D)
     (by
       intro G H i
       -- porting note: was `ext` in lean 3
+      -- Now `ext` can't see that `lan` is a colimit.
+      -- Uncertain whether it makes sense to add another `@[ext]` lemma.
+      -- See https://github.com/leanprover-community/mathlib4/issues/5229
       apply colimit.hom_ext
       intro j
       simp only [Functor.comp_map, Functor.mapIso_refl, evaluation_obj_map, whiskeringLeft_obj_map,
diff --git a/Mathlib/CategoryTheory/Idempotents/Basic.lean b/Mathlib/CategoryTheory/Idempotents/Basic.lean
index 3d70e29244758..7878f7238e397 100644
--- a/Mathlib/CategoryTheory/Idempotents/Basic.lean
+++ b/Mathlib/CategoryTheory/Idempotents/Basic.lean
@@ -89,7 +89,7 @@ theorem isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent :
     haveI : HasEqualizer (𝟙 X) p := h X p hp
     refine' ⟨equalizer (𝟙 X) p, equalizer.ι (𝟙 X) p,
       equalizer.lift p (show p ≫ 𝟙 X = p ≫ p by rw [hp, comp_id]), _, equalizer.lift_ι _ _⟩
-    apply equalizer.hom_ext
+    ext
     simp only [assoc, limit.lift_π, Eq.ndrec, id_eq, eq_mpr_eq_cast, Fork.ofι_pt,
       Fork.ofι_π_app, id_comp]
     rw [← equalizer.condition, comp_id]
@@ -131,7 +131,7 @@ instance (priority := 100) isIdempotentComplete_of_abelian (D : Type _) [Categor
 variable {C}
 
 theorem split_imp_of_iso {X X' : C} (φ : X ≅ X') (p : X ⟶ X) (p' : X' ⟶ X')
-    (hpp' : p ≫ φ.hom = φ.hom ≫ p') 
+    (hpp' : p ≫ φ.hom = φ.hom ≫ p')
     (h : ∃ (Y : C) (i : Y ⟶ X) (e : X ⟶ Y), i ≫ e = 𝟙 Y ∧ e ≫ i = p) :
     ∃ (Y' : C) (i' : Y' ⟶ X') (e' : X' ⟶ Y'), i' ≫ e' = 𝟙 Y' ∧ e' ≫ i' = p' := by
   rcases h with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
diff --git a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
index ef1c8eb9f5e5b..64a7aa516ed38 100644
--- a/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
+++ b/Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean
@@ -72,9 +72,7 @@ instance functor_category_isIdempotentComplete [IsIdempotentComplete C] :
     { obj := fun j => Limits.equalizer (𝟙 _) (p.app j)
       map := fun {j j'} φ =>
         equalizer.lift (Limits.equalizer.ι (𝟙 _) (p.app j) ≫ F.map φ)
-          (by rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id])
-      map_id := fun _ => equalizer.hom_ext (by simp)
-      map_comp := fun _ _ => equalizer.hom_ext (by simp) }
+          (by rw [comp_id, assoc, p.naturality φ, ← assoc, ← Limits.equalizer.condition, comp_id]) }
   let i : Y ⟶ F :=
     { app := fun j => equalizer.ι _ _
       naturality := fun _ _ _ => by rw [equalizer.lift_ι] }
diff --git a/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean b/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean
index 1c4c825db55f1..fb98a14007ba9 100644
--- a/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean
+++ b/Mathlib/CategoryTheory/Limits/ConcreteCategory.lean
@@ -162,9 +162,8 @@ section Colimits
 theorem cokernel_funext {C : Type _} [Category C] [HasZeroMorphisms C] [ConcreteCategory C]
     {M N K : C} {f : M ⟶ N} [HasCokernel f] {g h : cokernel f ⟶ K}
     (w : ∀ n : N, g (cokernel.π f n) = h (cokernel.π f n)) : g = h := by
-  apply coequalizer.hom_ext
-  apply ConcreteCategory.hom_ext _ _
-  simpa using w
+  ext x
+  simpa using w x
 #align category_theory.limits.cokernel_funext CategoryTheory.Limits.cokernel_funext
 
 variable {C : Type u} [Category.{v} C] [ConcreteCategory.{v} C] {J : Type v} [SmallCategory J]
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
index 8093d4e0c2229..b6ea529459a76 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
+++ b/Mathlib/CategoryTheory/Limits/Constructions/Equalizers.lean
@@ -73,8 +73,7 @@ def equalizerCone (F : WalkingParallelPair ⥤ C) : Cone F :=
 def equalizerConeIsLimit (F : WalkingParallelPair ⥤ C) : IsLimit (equalizerCone F) where
   lift := by
     intro c; apply pullback.lift (c.π.app _) (c.π.app _)
-    apply limit.hom_ext
-    rintro (_ | _) <;> simp
+    ext <;> simp
   fac := by rintro c (_ | _) <;> simp
   uniq := by
     intro c _ J
@@ -129,7 +128,7 @@ def preservesEqualizersOfPreservesPullbacksAndBinaryProducts [HasBinaryProducts
           rw [Iso.eq_comp_inv]
           have := h WalkingParallelPair.zero
           dsimp [equalizerCone] at this
-          apply pullback.hom_ext <;>
+          ext <;>
             simp only [PreservesPullback.iso_hom_snd, Category.assoc,
               PreservesPullback.iso_hom_fst, pullback.lift_fst, pullback.lift_snd,
               Category.comp_id, ← pullbackFst_eq_pullback_snd, ← this] }⟩
@@ -172,8 +171,7 @@ def coequalizerCocone (F : WalkingParallelPair ⥤ C) : Cocone F :=
 def coequalizerCoconeIsColimit (F : WalkingParallelPair ⥤ C) : IsColimit (coequalizerCocone F) where
   desc := by
     intro c; apply pushout.desc (c.ι.app _) (c.ι.app _)
-    apply colimit.hom_ext
-    rintro (_ | _) <;> simp
+    ext <;> simp
   fac := by rintro c (_ | _) <;> simp
   uniq := by
     intro c m J
@@ -232,7 +230,7 @@ def preservesCoequalizersOfPreservesPushoutsAndBinaryCoproducts [HasBinaryCoprod
           rw [Iso.eq_inv_comp]
           have := h WalkingParallelPair.one
           dsimp [coequalizerCocone] at this
-          apply pushout.hom_ext <;>
+          ext <;>
             simp only [PreservesPushout.inl_iso_hom_assoc, Category.id_comp, pushout.inl_desc,
               pushout.inr_desc, PreservesPushout.inr_iso_hom_assoc, ← pushoutInl_eq_pushout_inr, ←
               this] }⟩
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean b/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
index 888d9cd51e30b..e625422d6df7f 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Constructions/Pullbacks.lean
@@ -43,8 +43,7 @@ theorem hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair {C : Type u} [
               rw [← Category.assoc, limit.lift_π, ← Category.assoc, limit.lift_π];
                 exact PullbackCone.condition _)
           (by simp) (by simp) fun s m h₁ h₂ => by
-          apply equalizer.hom_ext
-          apply prod.hom_ext
+          ext
           · dsimp; simpa using h₁
           · simpa using h₂ }
 #align category_theory.limits.has_limit_cospan_of_has_limit_pair_of_has_limit_parallel_pair CategoryTheory.Limits.hasLimit_cospan_of_hasLimit_pair_of_hasLimit_parallelPair
@@ -82,8 +81,7 @@ theorem hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair {C : Type
             rw [Category.assoc, colimit.ι_desc, Category.assoc, colimit.ι_desc]
             exact PushoutCocone.condition _)
           (by simp) (by simp) fun s m h₁ h₂ => by
-          apply coequalizer.hom_ext
-          apply coprod.hom_ext
+          ext
           · simpa using h₁
           · simpa using h₂ }
 #align category_theory.limits.has_colimit_span_of_has_colimit_pair_of_has_colimit_parallel_pair CategoryTheory.Limits.hasColimit_span_of_hasColimit_pair_of_hasColimit_parallelPair
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 5343d7d842747..c4f16b81426d8 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -309,7 +309,7 @@ theorem colimit_pre_is_iso_aux {t : Cocone G} (P : IsColimit t) :
   dsimp [isColimitWhiskerEquiv]
   apply P.hom_ext
   intro j
-  dsimp; simp
+  simp
 #align category_theory.functor.final.colimit_pre_is_iso_aux CategoryTheory.Functor.Final.colimit_pre_is_iso_aux
 
 instance colimit_pre_isIso [HasColimit G] : IsIso (colimit.pre G F) := by
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index d8fe061c92e2a..f3e01a2bd8e01 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -1108,7 +1108,7 @@ theorem colimit.ι_map (j : J) : colimit.ι F j ≫ colim.map α = α.app j ≫
 @[simp] -- Porting note: proof adjusted to account for @[simps] on all fields of colim
 theorem colimit.map_desc (c : Cocone G) :
     colimMap α ≫ colimit.desc G c = colimit.desc F ((Cocones.precompose α).obj c) := by
-  apply Limits.colimit.hom_ext; intro j
+  ext j
   simp [← assoc, colimit.ι_map, assoc, colimit.ι_desc, colimit.ι_desc]
 #align category_theory.limits.colimit.map_desc CategoryTheory.Limits.colimit.map_desc
 
diff --git a/Mathlib/CategoryTheory/Limits/Over.lean b/Mathlib/CategoryTheory/Limits/Over.lean
index 51219cfa84549..6bc01bc7ee9d5 100644
--- a/Mathlib/CategoryTheory/Limits/Over.lean
+++ b/Mathlib/CategoryTheory/Limits/Over.lean
@@ -104,6 +104,7 @@ def mapPullbackAdj {A B : C} (f : A ⟶ B) : Over.map f ⊣ pullback f :=
             dsimp
             simp
           right_inv := fun Y => by
+            -- TODO: It would be nice to replace the next two lines with just `ext`.
             apply OverMorphism.ext
             apply pullback.hom_ext
             . dsimp
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
index 37ba35665d8e0..489d4fb949750 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Limits.lean
@@ -89,7 +89,7 @@ def preservesLimitNatIso : lim ⋙ G ≅ (whiskeringRight J C D).obj G ⋙ lim :
   NatIso.ofComponents (fun F => preservesLimitIso G F)
     (by
       intro _ _ f
-      apply Limits.limit.hom_ext; intro j
+      apply limit.hom_ext; intro j
       dsimp
       simp only [preservesLimitsIso_hom_π, whiskerRight_app, limMap_π, Category.assoc,
         preservesLimitsIso_hom_π_assoc, ← G.map_comp])
@@ -147,7 +147,7 @@ def preservesColimitNatIso : colim ⋙ G ≅ (whiskeringRight J C D).obj G ⋙ c
     (by
       intro _ _ f
       rw [← Iso.inv_comp_eq, ← Category.assoc, ← Iso.eq_comp_inv]
-      apply Limits.colimit.hom_ext; intro j
+      apply colimit.hom_ext; intro j
       dsimp
       erw [ι_colimMap_assoc]
       simp only [ι_preservesColimitsIso_inv, whiskerRight_app, Category.assoc,
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
index 3b6de6b8f4137..1979877326616 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
@@ -421,7 +421,7 @@ theorem biproduct.map_lift_mapBiprod (g : ∀ j, W ⟶ f j) :
     -- Porting note: twice we need haveI to tell Lean about hasBiproduct_of_preserves F f
     haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     F.map (biproduct.lift g) ≫ (F.mapBiproduct f).hom = biproduct.lift fun j => F.map (g j) := by
-  apply biproduct.hom_ext; intro j'
+  ext j
   dsimp [Function.comp]
   haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
   simp only [mapBiproduct_hom, Category.assoc, biproduct.lift_π, ← F.map_comp]
@@ -431,7 +431,7 @@ theorem biproduct.mapBiproduct_inv_map_desc (g : ∀ j, f j ⟶ W) :
     -- Porting note: twice we need haveI to tell Lean about hasBiproduct_of_preserves F f
     haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
     (F.mapBiproduct f).inv ≫ F.map (biproduct.desc g) = biproduct.desc fun j => F.map (g j) := by
-  apply biproduct.hom_ext'; intro j
+  ext j
   dsimp [Function.comp]
   haveI : HasBiproduct fun j => F.obj (f j) := hasBiproduct_of_preserves F f
   simp only [mapBiproduct_inv, ← Category.assoc, biproduct.ι_desc ,← F.map_comp]
@@ -450,7 +450,7 @@ variable (X Y : C) [HasBinaryBiproduct X Y] [PreservesBinaryBiproduct X Y F] {W
 
 theorem biprod.map_lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
     F.map (biprod.lift f g) ≫ (F.mapBiprod X Y).hom = biprod.lift (F.map f) (F.map g) := by
-  apply biprod.hom_ext <;> simp [mapBiprod, ← F.map_comp]
+  ext <;> simp [mapBiprod, ← F.map_comp]
 #align category_theory.limits.biprod.map_lift_map_biprod CategoryTheory.Limits.biprod.map_lift_mapBiprod
 
 theorem biprod.lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
@@ -460,7 +460,7 @@ theorem biprod.lift_mapBiprod (f : W ⟶ X) (g : W ⟶ Y) :
 
 theorem biprod.mapBiprod_inv_map_desc (f : X ⟶ W) (g : Y ⟶ W) :
     (F.mapBiprod X Y).inv ≫ F.map (biprod.desc f g) = biprod.desc (F.map f) (F.map g) := by
-  apply biprod.hom_ext' <;> simp [mapBiprod, ← F.map_comp]
+  ext <;> simp [mapBiprod, ← F.map_comp]
 #align category_theory.limits.biprod.map_biprod_inv_map_desc CategoryTheory.Limits.biprod.mapBiprod_inv_map_desc
 
 theorem biprod.mapBiprod_hom_desc (f : X ⟶ W) (g : Y ⟶ W) :
diff --git a/Mathlib/CategoryTheory/Limits/Presheaf.lean b/Mathlib/CategoryTheory/Limits/Presheaf.lean
index 48caeee52ff37..c797e4ef7d5b9 100644
--- a/Mathlib/CategoryTheory/Limits/Presheaf.lean
+++ b/Mathlib/CategoryTheory/Limits/Presheaf.lean
@@ -149,6 +149,7 @@ theorem extendAlongYoneda_obj (P : Cᵒᵖ ⥤ Type u₁) :
 -- stuck (and hence can see through definitional equalities). The previous lemma shows that
 -- `(extendAlongYoneda A).obj P` is definitionally a colimit, and the ext lemma is just
 -- a special case of `CategoryTheory.Limits.colimit.hom_ext`.
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext] lemma extendAlongYoneda_obj.hom_ext {P : Cᵒᵖ ⥤ Type u₁}
     {f f' : (extendAlongYoneda A).obj P ⟶ X}
     (w : ∀ j, colimit.ι ((CategoryOfElements.π P).leftOp ⋙ A) j ≫ f =
@@ -221,8 +222,7 @@ noncomputable def isExtensionAlongYoneda :
       -- porting note: this is slightly different to the `change` in mathlib3 which
       -- didn't work
       change (colimit.desc _ _ ≫ _) = colimit.desc _ _ ≫ _
-      apply colimit.hom_ext
-      intro j
+      ext
       rw [colimit.ι_desc_assoc, colimit.ι_desc_assoc]
       change (colimit.ι _ _ ≫ 𝟙 _) ≫ colimit.desc _ _ = _
       rw [comp_id, colimit.ι_desc]
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
index ecdecdc34603d..dad6ad3d87348 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
@@ -709,7 +709,7 @@ section ProdLemmas
 -- Making the reassoc version of this a simp lemma seems to be more harmful than helpful.
 @[reassoc, simp]
 theorem prod.comp_lift {V W X Y : C} [HasBinaryProduct X Y] (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y) :
-    f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h) := by apply prod.hom_ext; simp; simp
+    f ≫ prod.lift g h = prod.lift (f ≫ g) (f ≫ h) := by ext <;> simp
 #align category_theory.limits.prod.comp_lift CategoryTheory.Limits.prod.comp_lift
 #align category_theory.limits.prod.comp_lift_assoc CategoryTheory.Limits.prod.comp_lift_assoc
 
@@ -733,18 +733,18 @@ theorem prod.map_snd {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z]
 
 @[simp]
 theorem prod.map_id_id {X Y : C} [HasBinaryProduct X Y] : prod.map (𝟙 X) (𝟙 Y) = 𝟙 _ := by
-  apply prod.hom_ext; simp; simp
+  ext <;> simp
 #align category_theory.limits.prod.map_id_id CategoryTheory.Limits.prod.map_id_id
 
 @[simp]
 theorem prod.lift_fst_snd {X Y : C} [HasBinaryProduct X Y] :
-    prod.lift prod.fst prod.snd = 𝟙 (X ⨯ Y) := by apply prod.hom_ext; simp; simp
+    prod.lift prod.fst prod.snd = 𝟙 (X ⨯ Y) := by ext <;> simp
 #align category_theory.limits.prod.lift_fst_snd CategoryTheory.Limits.prod.lift_fst_snd
 
 @[reassoc (attr := simp)]
 theorem prod.lift_map {V W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z] (f : V ⟶ W)
     (g : V ⟶ X) (h : W ⟶ Y) (k : X ⟶ Z) :
-    prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k) := by apply prod.hom_ext; simp; simp
+    prod.lift f g ≫ prod.map h k = prod.lift (f ≫ h) (g ≫ k) := by ext <;> simp
 #align category_theory.limits.prod.lift_map CategoryTheory.Limits.prod.lift_map
 #align category_theory.limits.prod.lift_map_assoc CategoryTheory.Limits.prod.lift_map_assoc
 
@@ -761,7 +761,7 @@ theorem prod.lift_fst_comp_snd_comp {W X Y Z : C} [HasBinaryProduct W Y] [HasBin
 @[reassoc (attr := simp)]
 theorem prod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryProduct A₁ B₁] [HasBinaryProduct A₂ B₂]
     [HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
-    prod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k) := by apply prod.hom_ext; simp; simp
+    prod.map f g ≫ prod.map h k = prod.map (f ≫ h) (g ≫ k) := by ext <;> simp
 #align category_theory.limits.prod.map_map CategoryTheory.Limits.prod.map_map
 #align category_theory.limits.prod.map_map_assoc CategoryTheory.Limits.prod.map_map_assoc
 
@@ -804,7 +804,7 @@ instance isIso_prod {W X Y Z : C} [HasBinaryProduct W X] [HasBinaryProduct Y Z]
 instance prod.map_mono {C : Type _} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
     [Mono g] [HasBinaryProduct W X] [HasBinaryProduct Y Z] : Mono (prod.map f g) :=
   ⟨fun i₁ i₂ h => by
-    apply prod.hom_ext
+    ext
     · rw [← cancel_mono f]
       simpa using congr_arg (fun f => f ≫ prod.fst) h
     · rw [← cancel_mono g]
@@ -841,7 +841,7 @@ section CoprodLemmas
 @[simp] -- Porting note: removing reassoc tag since result is not hygienic (two h's)
 theorem coprod.desc_comp {V W X Y : C} [HasBinaryCoproduct X Y] (f : V ⟶ W) (g : X ⟶ V)
     (h : Y ⟶ V) : coprod.desc g h ≫ f = coprod.desc (g ≫ f) (h ≫ f) := by
-  apply coprod.hom_ext; simp; simp
+  ext <;> simp
 #align category_theory.limits.coprod.desc_comp CategoryTheory.Limits.coprod.desc_comp
 
 -- Porting note: hand generated reassoc here. Simp can prove it
@@ -870,12 +870,12 @@ theorem coprod.inr_map {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduc
 
 @[simp]
 theorem coprod.map_id_id {X Y : C} [HasBinaryCoproduct X Y] : coprod.map (𝟙 X) (𝟙 Y) = 𝟙 _ := by
-  apply coprod.hom_ext; simp; simp
+  ext <;> simp
 #align category_theory.limits.coprod.map_id_id CategoryTheory.Limits.coprod.map_id_id
 
 @[simp]
 theorem coprod.desc_inl_inr {X Y : C} [HasBinaryCoproduct X Y] :
-    coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y) := by apply coprod.hom_ext; simp; simp
+    coprod.desc coprod.inl coprod.inr = 𝟙 (X ⨿ Y) := by ext <;> simp
 #align category_theory.limits.coprod.desc_inl_inr CategoryTheory.Limits.coprod.desc_inl_inr
 
 -- The simp linter says simp can prove the reassoc version of this lemma.
@@ -883,7 +883,7 @@ theorem coprod.desc_inl_inr {X Y : C} [HasBinaryCoproduct X Y] :
 theorem coprod.map_desc {S T U V W : C} [HasBinaryCoproduct U W] [HasBinaryCoproduct T V]
     (f : U ⟶ S) (g : W ⟶ S) (h : T ⟶ U) (k : V ⟶ W) :
     coprod.map h k ≫ coprod.desc f g = coprod.desc (h ≫ f) (k ≫ g) := by
-  apply coprod.hom_ext; simp; simp
+  ext <;> simp
 #align category_theory.limits.coprod.map_desc CategoryTheory.Limits.coprod.map_desc
 #align category_theory.limits.coprod.map_desc_assoc CategoryTheory.Limits.coprod.map_desc_assoc
 
@@ -901,7 +901,7 @@ theorem coprod.desc_comp_inl_comp_inr {W X Y Z : C} [HasBinaryCoproduct W Y]
 theorem coprod.map_map {A₁ A₂ A₃ B₁ B₂ B₃ : C} [HasBinaryCoproduct A₁ B₁] [HasBinaryCoproduct A₂ B₂]
     [HasBinaryCoproduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃) :
     coprod.map f g ≫ coprod.map h k = coprod.map (f ≫ h) (g ≫ k) := by
-  apply coprod.hom_ext; simp; simp
+  ext <;> simp
 #align category_theory.limits.coprod.map_map CategoryTheory.Limits.coprod.map_map
 #align category_theory.limits.coprod.map_map_assoc CategoryTheory.Limits.coprod.map_map_assoc
 
@@ -944,7 +944,7 @@ instance isIso_coprod {W X Y Z : C} [HasBinaryCoproduct W X] [HasBinaryCoproduct
 instance coprod.map_epi {C : Type _} [Category C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
     [Epi g] [HasBinaryCoproduct W X] [HasBinaryCoproduct Y Z] : Epi (coprod.map f g) :=
   ⟨fun i₁ i₂ h => by
-    apply coprod.hom_ext
+    ext
     · rw [← cancel_epi f]
       simpa using congr_arg (fun f => coprod.inl ≫ f) h
     · rw [← cancel_epi g]
@@ -1048,14 +1048,6 @@ theorem prod.symmetry (P Q : C) [HasBinaryProduct P Q] [HasBinaryProduct Q P] :
 def prod.associator [HasBinaryProducts C] (P Q R : C) : (P ⨯ Q) ⨯ R ≅ P ⨯ Q ⨯ R where
   hom := prod.lift (prod.fst ≫ prod.fst) (prod.lift (prod.fst ≫ prod.snd) prod.snd)
   inv := prod.lift (prod.lift prod.fst (prod.snd ≫ prod.fst)) (prod.snd ≫ prod.snd)
-  hom_inv_id := by
-    apply prod.hom_ext
-    · apply prod.hom_ext; simp; simp
-    · simp
-  inv_hom_id := by
-    apply prod.hom_ext
-    · simp
-    · apply prod.hom_ext; simp; simp
 #align category_theory.limits.prod.associator CategoryTheory.Limits.prod.associator
 
 @[reassoc]
@@ -1083,10 +1075,7 @@ variable [HasTerminal C]
 def prod.leftUnitor (P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P where
   hom := prod.snd
   inv := prod.lift (terminal.from P) (𝟙 _)
-  hom_inv_id := by
-    apply prod.hom_ext
-    · simp
-    · simp
+  hom_inv_id := by apply prod.hom_ext <;> simp
   inv_hom_id := by simp
 #align category_theory.limits.prod.left_unitor CategoryTheory.Limits.prod.leftUnitor
 
@@ -1095,10 +1084,7 @@ def prod.leftUnitor (P : C) [HasBinaryProduct (⊤_ C) P] : (⊤_ C) ⨯ P ≅ P
 def prod.rightUnitor (P : C) [HasBinaryProduct P (⊤_ C)] : P ⨯ ⊤_ C ≅ P where
   hom := prod.fst
   inv := prod.lift (𝟙 _) (terminal.from P)
-  hom_inv_id := by
-    apply prod.hom_ext
-    · simp
-    · simp
+  hom_inv_id := by apply prod.hom_ext <;> simp
   inv_hom_id := by simp
 #align category_theory.limits.prod.right_unitor CategoryTheory.Limits.prod.rightUnitor
 
@@ -1133,7 +1119,7 @@ theorem prod_rightUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
 theorem prod.triangle [HasBinaryProducts C] (X Y : C) :
     (prod.associator X (⊤_ C) Y).hom ≫ prod.map (𝟙 X) (prod.leftUnitor Y).hom =
       prod.map (prod.rightUnitor X).hom (𝟙 Y) :=
-  by dsimp; apply prod.hom_ext; simp; simp;
+  by ext <;> simp
 #align category_theory.limits.prod.triangle CategoryTheory.Limits.prod.triangle
 
 end
@@ -1167,14 +1153,6 @@ theorem coprod.symmetry (P Q : C) : (coprod.braiding P Q).hom ≫ (coprod.braidi
 def coprod.associator (P Q R : C) : (P ⨿ Q) ⨿ R ≅ P ⨿ Q ⨿ R where
   hom := coprod.desc (coprod.desc coprod.inl (coprod.inl ≫ coprod.inr)) (coprod.inr ≫ coprod.inr)
   inv := coprod.desc (coprod.inl ≫ coprod.inl) (coprod.desc (coprod.inr ≫ coprod.inl) coprod.inr)
-  hom_inv_id := by
-    apply coprod.hom_ext
-    · apply coprod.hom_ext; simp; simp
-    · simp
-  inv_hom_id := by
-    apply coprod.hom_ext
-    · simp
-    · apply coprod.hom_ext; simp; simp
 #align category_theory.limits.coprod.associator CategoryTheory.Limits.coprod.associator
 
 theorem coprod.pentagon (W X Y Z : C) :
@@ -1198,10 +1176,7 @@ variable [HasInitial C]
 def coprod.leftUnitor (P : C) : (⊥_ C) ⨿ P ≅ P where
   hom := coprod.desc (initial.to P) (𝟙 _)
   inv := coprod.inr
-  hom_inv_id := by
-    apply coprod.hom_ext
-    · simp
-    · simp
+  hom_inv_id := by apply coprod.hom_ext <;> simp
   inv_hom_id := by simp
 #align category_theory.limits.coprod.left_unitor CategoryTheory.Limits.coprod.leftUnitor
 
@@ -1210,17 +1185,14 @@ def coprod.leftUnitor (P : C) : (⊥_ C) ⨿ P ≅ P where
 def coprod.rightUnitor (P : C) : P ⨿ ⊥_ C ≅ P where
   hom := coprod.desc (𝟙 _) (initial.to P)
   inv := coprod.inl
-  hom_inv_id := by
-    apply coprod.hom_ext
-    · simp
-    · simp
+  hom_inv_id := by apply coprod.hom_ext <;> simp
   inv_hom_id := by simp
 #align category_theory.limits.coprod.right_unitor CategoryTheory.Limits.coprod.rightUnitor
 
 theorem coprod.triangle (X Y : C) :
     (coprod.associator X (⊥_ C) Y).hom ≫ coprod.map (𝟙 X) (coprod.leftUnitor Y).hom =
       coprod.map (coprod.rightUnitor X).hom (𝟙 Y) :=
-  by dsimp; apply coprod.hom_ext; simp; simp
+  by ext <;> simp
 #align category_theory.limits.coprod.triangle CategoryTheory.Limits.coprod.triangle
 
 end
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
index fced0f64d255c..c0be6d13e0dd2 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -460,7 +460,9 @@ abbrev biproduct.map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀
     (Discrete.natTrans fun j => p j.as)
 #align category_theory.limits.biproduct.map' CategoryTheory.Limits.biproduct.map'
 
-@[ext]
+-- We put this at slightly higher priority than `biproduct.hom_ext'`,
+-- to get the matrix indices in the "right" order.
+@[ext 1001]
 theorem biproduct.hom_ext {f : J → C} [HasBiproduct f] {Z : C} (g h : Z ⟶ ⨁ f)
     (w : ∀ j, g ≫ biproduct.π f j = h ≫ biproduct.π f j) : g = h :=
   (biproduct.isLimit f).hom_ext fun j => w j.as
@@ -508,12 +510,11 @@ theorem biproduct.isoCoproduct_hom {f : J → C} [HasBiproduct f] :
 
 theorem biproduct.map_eq_map' {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p : ∀ b, f b ⟶ g b) :
     biproduct.map p = biproduct.map' p := by
-  apply biproduct.hom_ext'; intro j
-  apply biproduct.hom_ext; intro j'
+  ext
   dsimp
-  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map, Limits.IsLimit.map_π, Category.assoc,
-    ← Bicone.toCone_π_app_mk, ← biproduct.bicone_π, ← Bicone.toCocone_ι_app_mk, ←
-    biproduct.bicone_ι]
+  simp only [Discrete.natTrans_app, Limits.IsColimit.ι_map_assoc, Limits.IsLimit.map_π,
+    Category.assoc, ← Bicone.toCone_π_app_mk, ← biproduct.bicone_π, ← Bicone.toCocone_ι_app_mk,
+    ← biproduct.bicone_ι]
   dsimp
   rw [biproduct.ι_π_assoc, biproduct.ι_π]
   split_ifs with h
@@ -601,7 +602,7 @@ theorem biproduct.fromSubtype_eq_lift [DecidablePred p] :
 @[reassoc] -- Porting note: both version solved using simp
 theorem biproduct.fromSubtype_π_subtype (j : Subtype p) :
     biproduct.fromSubtype f p ≫ biproduct.π f j = biproduct.π (Subtype.restrict p f) j := by
-  apply biproduct.hom_ext'; intro i
+  ext
   rw [biproduct.fromSubtype, biproduct.ι_desc_assoc, biproduct.ι_π, biproduct.ι_π]
   split_ifs with h₁ h₂ h₂
   exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
@@ -617,7 +618,7 @@ theorem biproduct.toSubtype_π (j : Subtype p) :
 theorem biproduct.ι_toSubtype [DecidablePred p] (j : J) :
     biproduct.ι f j ≫ biproduct.toSubtype f p =
       if h : p j then biproduct.ι (Subtype.restrict p f) ⟨j, h⟩ else 0 := by
-  apply biproduct.hom_ext; intro i
+  ext i
   rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π]
   by_cases h : p j
   · rw [dif_pos h, biproduct.ι_π]
@@ -635,7 +636,7 @@ theorem biproduct.toSubtype_eq_desc [DecidablePred p] :
 @[reassoc] -- Porting note: simp can prove both versions
 theorem biproduct.ι_toSubtype_subtype (j : Subtype p) :
     biproduct.ι f j ≫ biproduct.toSubtype f p = biproduct.ι (Subtype.restrict p f) j := by
-  apply biproduct.hom_ext; intro i
+  ext
   rw [biproduct.toSubtype, Category.assoc, biproduct.lift_π, biproduct.ι_π, biproduct.ι_π]
   split_ifs with h₁ h₂ h₂
   exacts [rfl, False.elim (h₂ (Subtype.ext h₁)), False.elim (h₁ (congr_arg Subtype.val h₂)), rfl]
@@ -740,10 +741,10 @@ def kernelForkBiproductToSubtype (p : Set K) : LimitCone (parallelPair (biproduc
   cone :=
     KernelFork.ofι (biproduct.fromSubtype f (pᶜ))
       (by
-        apply biproduct.hom_ext'; intro j
-        apply biproduct.hom_ext; intro k
-        simp only [biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype, comp_zero, zero_comp]
-        erw [dif_neg j.2]
+        ext j k
+        simp only [Category.assoc, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype_assoc,
+          comp_zero, zero_comp]
+        erw [dif_neg k.2]
         simp only [zero_comp])
   isLimit :=
     KernelFork.IsLimit.ofι _ _ (fun {W} g _ => g ≫ biproduct.toSubtype f (pᶜ))
@@ -777,13 +778,12 @@ def cokernelCoforkBiproductFromSubtype (p : Set K) :
   cocone :=
     CokernelCofork.ofπ (biproduct.toSubtype f (pᶜ))
       (by
-        apply biproduct.hom_ext'; intro j
-        apply biproduct.hom_ext; intro k
-        simp only [Pi.compl_apply, biproduct.ι_fromSubtype_assoc, biproduct.ι_toSubtype,
-          comp_zero, zero_comp]
+        ext j k
+        simp only [Category.assoc, Pi.compl_apply, biproduct.ι_fromSubtype_assoc,
+          biproduct.ι_toSubtype_assoc, comp_zero, zero_comp]
         rw [dif_neg]
         simp only [zero_comp]
-        exact not_not.mpr j.2)
+        exact not_not.mpr k.2)
   isColimit :=
     CokernelCofork.IsColimit.ofπ _ _ (fun {W} g _ => biproduct.fromSubtype f (pᶜ) ≫ g)
       (by
@@ -1439,13 +1439,13 @@ def biprod.isoProd (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨯ Y :=
 @[simp]
 theorem biprod.isoProd_hom {X Y : C} [HasBinaryBiproduct X Y] :
     (biprod.isoProd X Y).hom = prod.lift biprod.fst biprod.snd := by
-      apply biprod.hom_ext' <;> apply prod.hom_ext <;> simp [biprod.isoProd]
+      ext <;> simp [biprod.isoProd]
 #align category_theory.limits.biprod.iso_prod_hom CategoryTheory.Limits.biprod.isoProd_hom
 
 @[simp]
 theorem biprod.isoProd_inv {X Y : C} [HasBinaryBiproduct X Y] :
     (biprod.isoProd X Y).inv = biprod.lift prod.fst prod.snd := by
-  apply biprod.hom_ext <;> simp [Iso.inv_comp_eq]
+  ext <;> simp [Iso.inv_comp_eq]
 #align category_theory.limits.biprod.iso_prod_inv CategoryTheory.Limits.biprod.isoProd_inv
 
 /-- The canonical isomorphism between the chosen biproduct and the chosen coproduct. -/
@@ -1456,18 +1456,18 @@ def biprod.isoCoprod (X Y : C) [HasBinaryBiproduct X Y] : X ⊞ Y ≅ X ⨿ Y :=
 @[simp]
 theorem biprod.isoCoprod_inv {X Y : C} [HasBinaryBiproduct X Y] :
     (biprod.isoCoprod X Y).inv = coprod.desc biprod.inl biprod.inr := by
-  apply biprod.hom_ext <;> apply coprod.hom_ext <;> simp [biprod.isoCoprod]
+  ext <;> simp [biprod.isoCoprod]
 #align category_theory.limits.biprod.iso_coprod_inv CategoryTheory.Limits.biprod.isoCoprod_inv
 
 @[simp]
 theorem biprod_isoCoprod_hom {X Y : C} [HasBinaryBiproduct X Y] :
     (biprod.isoCoprod X Y).hom = biprod.desc coprod.inl coprod.inr := by
-  apply biprod.hom_ext' <;> simp [← Iso.eq_comp_inv]
+  ext <;> simp [← Iso.eq_comp_inv]
 #align category_theory.limits.biprod_iso_coprod_hom CategoryTheory.Limits.biprod_isoCoprod_hom
 
 theorem biprod.map_eq_map' {W X Y Z : C} [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z]
     (f : W ⟶ Y) (g : X ⟶ Z) : biprod.map f g = biprod.map' f g := by
-  apply biprod.hom_ext' <;> apply biprod.hom_ext
+  ext
   · simp only [mapPair_left, IsColimit.ι_map, IsLimit.map_π, biprod.inl_fst_assoc,
       Category.assoc, ← BinaryBicone.toCone_π_app_left, ← BinaryBiproduct.bicone_fst, ←
       BinaryBicone.toCocone_ι_app_left, ← BinaryBiproduct.bicone_inl];
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
index 4afd63a3b003e..3eaf2748de519 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
@@ -277,7 +277,7 @@ theorem pullbackDiagonalMapIdIso_inv_snd_snd :
 theorem pullback.diagonal_comp (f : X ⟶ Y) (g : Y ⟶ Z) [HasPullback f f] [HasPullback g g]
     [HasPullback (f ≫ g) (f ≫ g)] :
     diagonal (f ≫ g) = diagonal f ≫ (pullbackDiagonalMapIdIso f f g).inv ≫ pullback.snd := by
-  apply pullback.hom_ext <;> simp
+  ext <;> simp
 #align category_theory.limits.pullback.diagonal_comp CategoryTheory.Limits.pullback.diagonal_comp
 
 theorem pullback_map_diagonal_isPullback :
@@ -287,9 +287,9 @@ theorem pullback_map_diagonal_isPullback :
       (pullback.map (f ≫ i) (g ≫ i) i i f g (𝟙 _) (Category.comp_id _) (Category.comp_id _)) := by
   apply IsPullback.of_iso_pullback _ (pullbackDiagonalMapIdIso f g i).symm
   · simp
-  · apply pullback.hom_ext <;> simp
+  · ext <;> simp
   · constructor
-    apply pullback.hom_ext <;> simp [condition]
+    ext <;> simp [condition]
 #align category_theory.limits.pullback_map_diagonal_is_pullback CategoryTheory.Limits.pullback_map_diagonal_isPullback
 
 /-- The diagonal object of `X ×[Z] Y ⟶ X` is isomorphic to `Δ_{Y/Z} ×[Z] X`. -/
@@ -360,7 +360,7 @@ theorem diagonal_pullback_fst {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) :
         ((baseChange f).map
               (Over.homMk (diagonal g) : Over.mk g ⟶ Over.mk (pullback.snd ≫ g))).left ≫
           (diagonalObjPullbackFstIso f g).inv := by
-  apply pullback.hom_ext <;> apply pullback.hom_ext <;> dsimp <;> simp
+  ext <;> dsimp <;> simp
 #align category_theory.limits.diagonal_pullback_fst CategoryTheory.Limits.diagonal_pullback_fst
 
 end
@@ -404,6 +404,8 @@ def pullbackFstFstIso {X Y S X' Y' S' : C} (f : X ⟶ S) (g : Y ⟶ S) (f' : X'
       (pullback.lift (pullback.map _ _ _ _ _ _ _ e₁ e₂) pullback.snd (pullback.lift_snd _ _ _))
       (by rw [pullback.lift_fst, pullback.lift_fst])
   hom_inv_id := by
+    -- We could use `ext` here to immediately descend to the leaf goals,
+    -- but it only obscures the structure.
     apply pullback.hom_ext
     . apply pullback.hom_ext
       . apply pullback.hom_ext
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
index b41600b376cf5..0d1a9f54ee1b3 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
@@ -915,7 +915,7 @@ theorem equalizer.isoSourceOfSelf_hom : (equalizer.isoSourceOfSelf f).hom = equa
 @[simp]
 theorem equalizer.isoSourceOfSelf_inv :
     (equalizer.isoSourceOfSelf f).inv = equalizer.lift (𝟙 X) (by simp) := by
-  apply equalizer.hom_ext
+  ext
   simp [equalizer.isoSourceOfSelf]
 #align category_theory.limits.equalizer.iso_source_of_self_inv CategoryTheory.Limits.equalizer.isoSourceOfSelf_inv
 
@@ -1100,7 +1100,7 @@ noncomputable def coequalizer.isoTargetOfSelf : coequalizer f f ≅ Y :=
 @[simp]
 theorem coequalizer.isoTargetOfSelf_hom :
     (coequalizer.isoTargetOfSelf f).hom = coequalizer.desc (𝟙 Y) (by simp) := by
-  apply coequalizer.hom_ext
+  ext
   simp [coequalizer.isoTargetOfSelf]
 #align category_theory.limits.coequalizer.iso_target_of_self_hom CategoryTheory.Limits.coequalizer.isoTargetOfSelf_hom
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean b/Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
index a704bc7dbb023..bf441f4868eac 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
@@ -184,8 +184,8 @@ protected theorem pullback {X Y Z A : C} {g : Y ⟶ Z} {a₁ a₂ : A ⟶ Y} (h
         (fun s m hm => _)⟩⟩
   . simp_rw [Category.assoc, ← pullback.condition, ← Category.assoc, s.condition]
   . simp only [assoc, lift_fst_assoc, pullback.condition]
-  . apply pullback.hom_ext <;> simp
-  . apply pullback.hom_ext
+  . ext <;> simp
+  . ext
     . simp [s.condition]
     . simp
   . apply pullback.hom_ext
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
index 6a9047f6ac9fd..0d87be0249675 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
@@ -222,7 +222,7 @@ section
 variable [HasKernel f]
 
 /-- The kernel of a morphism, expressed as the equalizer with the 0 morphism. -/
-abbrev kernel (f : X ⟶  Y) [HasKernel f] : C :=
+abbrev kernel (f : X ⟶ Y) [HasKernel f] : C :=
   equalizer f 0
 #align category_theory.limits.kernel CategoryTheory.Limits.kernel
 
@@ -258,7 +258,7 @@ theorem kernel.lift_ι {W : C} (k : W ⟶ X) (h : k ≫ f = 0) : kernel.lift f k
 
 @[simp]
 theorem kernel.lift_zero {W : C} {h} : kernel.lift f (0 : W ⟶ X) h = 0 := by
-  apply equalizer.hom_ext; simp
+  ext; simp
 #align category_theory.limits.kernel.lift_zero CategoryTheory.Limits.kernel.lift_zero
 
 instance kernel.lift_mono {W : C} (k : W ⟶ X) (h : k ≫ f = 0) [Mono k] : Mono (kernel.lift f k h) :=
@@ -299,7 +299,7 @@ theorem kernel.lift_map {X Y Z X' Y' Z' : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKer
     (f' : X' ⟶ Y') (g' : Y' ⟶ Z') [HasKernel g'] (w' : f' ≫ g' = 0) (p : X ⟶ X') (q : Y ⟶ Y')
     (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
     kernel.lift g f w ≫ kernel.map g g' q r h₂ = p ≫ kernel.lift g' f' w' := by
-  apply equalizer.hom_ext; simp [h₁]
+  ext; simp [h₁]
 #align category_theory.limits.kernel.lift_map CategoryTheory.Limits.kernel.lift_map
 
 /-- A commuting square of isomorphisms induces an isomorphism of kernels. -/
@@ -312,8 +312,6 @@ def kernel.mapIso {X' Y' : C} (f' : X' ⟶ Y') [HasKernel f'] (p : X ≅ X') (q
       (by
         refine' (cancel_mono q.hom).1 _
         simp [w])
-  hom_inv_id := by apply equalizer.hom_ext; simp
-  inv_hom_id := by apply equalizer.hom_ext; simp
 #align category_theory.limits.kernel.map_iso CategoryTheory.Limits.kernel.mapIso
 
 /-- Every kernel of the zero morphism is an isomorphism -/
@@ -337,7 +335,7 @@ theorem kernelZeroIsoSource_hom : kernelZeroIsoSource.hom = kernel.ι (0 : X ⟶
 @[simp]
 theorem kernelZeroIsoSource_inv :
     kernelZeroIsoSource.inv = kernel.lift (0 : X ⟶ Y) (𝟙 X) (by simp) := by
-  apply equalizer.hom_ext
+  ext
   simp [kernelZeroIsoSource]
 #align category_theory.limits.kernel_zero_iso_source_inv CategoryTheory.Limits.kernelZeroIsoSource_inv
 
@@ -414,8 +412,6 @@ def kernelCompMono {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasKernel f] [Mono g
         rw [← cancel_mono g]
         simp)
   inv := kernel.lift _ (kernel.ι _) (by simp)
-  hom_inv_id := by apply equalizer.hom_ext; simp
-  inv_hom_id := by apply equalizer.hom_ext; simp
 #align category_theory.limits.kernel_comp_mono CategoryTheory.Limits.kernelCompMono
 
 instance hasKernel_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel g] :
@@ -436,8 +432,6 @@ def kernelIsIsoComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [HasKernel
     kernel (f ≫ g) ≅ kernel g where
   hom := kernel.lift _ (kernel.ι _ ≫ f) (by simp)
   inv := kernel.lift _ (kernel.ι _ ≫ inv f) (by simp)
-  hom_inv_id := equalizer.hom_ext (by simp)
-  inv_hom_id := equalizer.hom_ext (by simp)
 #align category_theory.limits.kernel_is_iso_comp CategoryTheory.Limits.kernelIsIsoComp
 
 end
@@ -725,7 +719,7 @@ lemma colimit_ι_zero_cokernel_desc {C : Type _} [Category C]
 
 @[simp]
 theorem cokernel.desc_zero {W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0 := by
-  apply coequalizer.hom_ext; simp
+  ext; simp
 #align category_theory.limits.cokernel.desc_zero CategoryTheory.Limits.cokernel.desc_zero
 
 instance cokernel.desc_epi {W : C} (k : Y ⟶ W) (h : f ≫ k = 0) [Epi k] :
@@ -772,7 +766,7 @@ theorem cokernel.map_desc {X Y Z X' Y' Z' : C} (f : X ⟶ Y) [HasCokernel f] (g
     (w : f ≫ g = 0) (f' : X' ⟶ Y') [HasCokernel f'] (g' : Y' ⟶ Z') (w' : f' ≫ g' = 0) (p : X ⟶ X')
     (q : Y ⟶ Y') (r : Z ⟶ Z') (h₁ : f ≫ q = p ≫ f') (h₂ : g ≫ r = q ≫ g') :
     cokernel.map f f' p q h₁ ≫ cokernel.desc f' g' w' = cokernel.desc f g w ≫ r := by
-  apply coequalizer.hom_ext; simp [h₂]
+  ext; simp [h₂]
 #align category_theory.limits.cokernel.map_desc CategoryTheory.Limits.cokernel.map_desc
 
 /-- A commuting square of isomorphisms induces an isomorphism of cokernels. -/
@@ -783,8 +777,6 @@ def cokernel.mapIso {X' Y' : C} (f' : X' ⟶ Y') [HasCokernel f'] (p : X ≅ X')
   inv := cokernel.map f' f p.inv q.inv (by
           refine' (cancel_mono q.hom).1 _
           simp [w])
-  hom_inv_id := by apply coequalizer.hom_ext; simp
-  inv_hom_id := by apply coequalizer.hom_ext; simp
 #align category_theory.limits.cokernel.map_iso CategoryTheory.Limits.cokernel.mapIso
 
 /-- The cokernel of the zero morphism is an isomorphism -/
@@ -804,7 +796,7 @@ def cokernelZeroIsoTarget : cokernel (0 : X ⟶ Y) ≅ Y :=
 @[simp]
 theorem cokernelZeroIsoTarget_hom :
     cokernelZeroIsoTarget.hom = cokernel.desc (0 : X ⟶ Y) (𝟙 Y) (by simp) := by
-  apply coequalizer.hom_ext; simp [cokernelZeroIsoTarget]
+  ext; simp [cokernelZeroIsoTarget]
 #align category_theory.limits.cokernel_zero_iso_target_hom CategoryTheory.Limits.cokernelZeroIsoTarget_hom
 
 @[simp]
@@ -890,8 +882,6 @@ def cokernelCompIsIso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokernel f] [I
     cokernel (f ≫ g) ≅ cokernel f where
   hom := cokernel.desc _ (inv g ≫ cokernel.π f) (by simp)
   inv := cokernel.desc _ (g ≫ cokernel.π (f ≫ g)) (by rw [← Category.assoc, cokernel.condition])
-  hom_inv_id := by apply coequalizer.hom_ext; simp
-  inv_hom_id := by apply coequalizer.hom_ext; simp
 #align category_theory.limits.cokernel_comp_is_iso CategoryTheory.Limits.cokernelCompIsIso
 
 instance hasCokernel_epi_comp {X Y : C} (f : X ⟶ Y) [HasCokernel f] {W} (g : W ⟶ X) [Epi g] :
@@ -911,8 +901,6 @@ def cokernelEpiComp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [Epi f] [HasCokernel
       (by
         rw [← cancel_epi f, ← Category.assoc]
         simp)
-  hom_inv_id := by apply coequalizer.hom_ext; simp
-  inv_hom_id := by apply coequalizer.hom_ext; simp
 #align category_theory.limits.cokernel_epi_comp CategoryTheory.Limits.cokernelEpiComp
 
 end
@@ -995,8 +983,6 @@ def cokernelImageι {X Y : C} (f : X ⟶ Y) [HasImage f] [HasCokernel (image.ι
           congr
           rw [← image.fac f]
         rw [Category.assoc, cokernel.condition, HasZeroMorphisms.comp_zero])
-  hom_inv_id := by apply coequalizer.hom_ext; simp
-  inv_hom_id := by apply coequalizer.hom_ext; simp
 #align category_theory.limits.cokernel_image_ι CategoryTheory.Limits.cokernelImageι
 
 end HasImage
@@ -1111,7 +1097,7 @@ theorem map_lift_kernelComparison [HasKernel f] [HasKernel (G.map f)] {Z : C} {h
     (w : h ≫ f = 0) :
     G.map (kernel.lift _ h w) ≫ kernelComparison f G =
       kernel.lift _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) := by
-  apply equalizer.hom_ext; simp [← G.map_comp]
+  ext; simp [← G.map_comp]
 #align category_theory.limits.map_lift_kernel_comparison CategoryTheory.Limits.map_lift_kernelComparison
 
 @[reassoc]
@@ -1144,7 +1130,7 @@ theorem cokernelComparison_map_desc [HasCokernel f] [HasCokernel (G.map f)] {Z :
     (w : f ≫ h = 0) :
     cokernelComparison f G ≫ G.map (cokernel.desc _ h w) =
       cokernel.desc _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero]) := by
-  apply coequalizer.hom_ext; simp [← G.map_comp]
+  ext; simp [← G.map_comp]
 #align category_theory.limits.cokernel_comparison_map_desc CategoryTheory.Limits.cokernelComparison_map_desc
 
 @[reassoc]
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
index 4f512cefa3383..cd66f3a159851 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Multiequalizer.lean
@@ -491,7 +491,6 @@ noncomputable def toPiForkFunctor : Multifork I ⥤ Fork I.fstPiMap I.sndPiMap w
       w := by
         rintro (_ | _)
         · apply limit.hom_ext
-          dsimp
           simp
         · apply limit.hom_ext
           intros j
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
index ec01fe845e9b1..ed17978805bac 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -167,7 +167,7 @@ lemma Pi.hom_ext {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ f)
 
 @[ext 1050]
 lemma Sigma.hom_ext {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X)
-    (h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂ ) : g₁ = g₂ :=
+    (h : ∀ (b : β), Sigma.ι f b ≫ g₁ = Sigma.ι f b ≫ g₂) : g₁ = g₂ :=
   colimit.hom_ext (fun ⟨j⟩ => h j)
 
 /-- The fan constructed of the projections from the product is limiting. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean b/Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
index 7b50570c37e39..e5846b41fe72f 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/RegularMono.lean
@@ -211,7 +211,8 @@ instance coequalizerRegular (g h : X ⟶ Y) [HasColimit (parallelPair g h)] :
   w := coequalizer.condition g h
   isColimit :=
     Cofork.IsColimit.mk _ (fun s => colimit.desc _ s) (by simp) fun s m w => by
-      apply coequalizer.hom_ext; simp [← w]
+      apply coequalizer.hom_ext
+      simp [← w]
 #align category_theory.coequalizer_regular CategoryTheory.coequalizerRegular
 
 /-- Every split epimorphism is a regular epimorphism. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
index 847a13d1f3fb0..75f6c50a382d0 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
@@ -464,8 +464,7 @@ def limitConstTerminal {J : Type _} [Category J] {C : Type _} [Category C] [HasT
 theorem limitConstTerminal_inv_π {J : Type _} [Category J] {C : Type _} [Category C] [HasTerminal C]
     {j : J} :
     limitConstTerminal.inv ≫ limit.π ((CategoryTheory.Functor.const J).obj (⊤_ C)) j =
-      terminal.from _ := by
-  apply Limits.limit.hom_ext; aesop_cat
+      terminal.from _ := by aesop_cat
 #align category_theory.limits.limit_const_terminal_inv_π CategoryTheory.Limits.limitConstTerminal_inv_π
 
 instance {J : Type _} [Category J] {C : Type _} [Category C] [HasInitial C] :
@@ -491,7 +490,7 @@ def colimitConstInitial {J : Type _} [Category J] {C : Type _} [Category C] [Has
 theorem ι_colimitConstInitial_hom {J : Type _} [Category J] {C : Type _} [Category C] [HasInitial C]
     {j : J} :
     colimit.ι ((CategoryTheory.Functor.const J).obj (⊥_ C)) j ≫ colimitConstInitial.hom =
-      initial.to _ := by apply Limits.colimit.hom_ext; aesop_cat
+      initial.to _ := by aesop_cat
 #align category_theory.limits.ι_colimit_const_initial_hom CategoryTheory.Limits.ι_colimitConstInitial_hom
 
 /-- A category is an `InitialMonoClass` if the canonical morphism of an initial object is a
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Types.lean b/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
index d39440a1b1634..f08c6cefa18c4 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@@ -197,9 +197,9 @@ noncomputable def binaryProductIsoProd : binaryProductFunctor ≅ (prod.functor
   refine' NatIso.ofComponents (fun X => _) (fun _ => _)
   · refine' NatIso.ofComponents (fun Y => _) (fun _ => _)
     · exact ((limit.isLimit _).conePointUniqueUpToIso (binaryProductLimit X Y)).symm
-    . apply Limits.prod.hom_ext <;> dsimp <;> simp <;> rfl
+    . apply Limits.prod.hom_ext <;> simp <;> rfl
   . ext : 2
-    apply Limits.prod.hom_ext <;> dsimp <;> simp <;> rfl
+    apply Limits.prod.hom_ext <;> simp <;> rfl
 #align category_theory.limits.types.binary_product_iso_prod CategoryTheory.Limits.Types.binaryProductIsoProd
 
 /-- The sum type `X ⊕ Y` forms a cocone for the binary coproduct of `X` and `Y`. -/
diff --git a/Mathlib/CategoryTheory/Monad/Products.lean b/Mathlib/CategoryTheory/Monad/Products.lean
index fda3bdda6183c..66b28880e8e2a 100644
--- a/Mathlib/CategoryTheory/Monad/Products.lean
+++ b/Mathlib/CategoryTheory/Monad/Products.lean
@@ -81,14 +81,7 @@ def coalgebraEquivOver : Coalgebra (prodComonad X) ≌ Over X where
   functor := coalgebraToOver X
   inverse := overToCoalgebra X
   unitIso := NatIso.ofComponents fun A =>
-    Coalgebra.isoMk (Iso.refl _)
-      (prod.hom_ext
-        (by
-          dsimp
-          simp)
-        (by
-          dsimp
-          simpa using A.counit))
+    Coalgebra.isoMk (Iso.refl _) (prod.hom_ext (by simp) (by simpa using A.counit))
   counitIso := NatIso.ofComponents fun f => Over.isoMk (Iso.refl _)
 #align category_theory.coalgebra_equiv_over CategoryTheory.coalgebraEquivOver
 
@@ -139,13 +132,8 @@ def underToAlgebra : Under X ⥤ Monad.Algebra (coprodMonad X) where
 def algebraEquivUnder : Monad.Algebra (coprodMonad X) ≌ Under X where
   functor := algebraToUnder X
   inverse := underToAlgebra X
-  unitIso := NatIso.ofComponents
-    fun A =>
-      Monad.Algebra.isoMk (Iso.refl _)
-        (coprod.hom_ext (by aesop_cat)
-          (by
-            dsimp
-            simpa using A.unit.symm))
+  unitIso := NatIso.ofComponents fun A =>
+    Monad.Algebra.isoMk (Iso.refl _) (coprod.hom_ext (by simp) (by simpa using A.unit.symm))
   counitIso :=
     NatIso.ofComponents fun f => Under.isoMk (Iso.refl _)
 #align category_theory.algebra_equiv_under CategoryTheory.algebraEquivUnder
diff --git a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
index 5f7a93c7bbcf1..ebd76a9492aba 100644
--- a/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/CommMon_.lean
@@ -65,6 +65,7 @@ set_option linter.uppercaseLean3 false in
 
 -- porting note: added because `Mon_.Hom.ext` is not triggered automatically
 -- for morphisms in `CommMon_ C`
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma hom_ext {A B : CommMon_ C} (f g : A ⟶ B) (h : f.hom = g.hom) : f = g :=
   Mon_.Hom.ext _ _ h
diff --git a/Mathlib/CategoryTheory/Monoidal/Mod_.lean b/Mathlib/CategoryTheory/Monoidal/Mod_.lean
index b7343e754b90f..f6e63b3c009af 100644
--- a/Mathlib/CategoryTheory/Monoidal/Mod_.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Mod_.lean
@@ -77,6 +77,7 @@ instance : Category (Mod_ A) where
   comp f g := comp f g
 
 -- porting note: added because `Hom.ext` is not triggered automatically
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma hom_ext {M N : Mod_ A} (f₁ f₂ : M ⟶ N) (h : f₁.hom = f₂.hom) : f₁ = f₂ :=
   Hom.ext _ _ h
diff --git a/Mathlib/CategoryTheory/MorphismProperty.lean b/Mathlib/CategoryTheory/MorphismProperty.lean
index 9247416d6bea1..bb59cc3d06813 100644
--- a/Mathlib/CategoryTheory/MorphismProperty.lean
+++ b/Mathlib/CategoryTheory/MorphismProperty.lean
@@ -224,7 +224,7 @@ theorem StableUnderBaseChange.baseChange_map [HasPullbacks C] {P : MorphismPrope
     pullbackRightPullbackFstIso Y.hom f g.left ≪≫
       pullback.congrHom (g.w.trans (Category.comp_id _)) rfl
   have : e.inv ≫ pullback.snd = ((baseChange f).map g).left := by
-    apply pullback.hom_ext <;> dsimp <;> simp
+    ext <;> dsimp <;> simp
   rw [← this, hP.respectsIso.cancel_left_isIso]
   exact hP.snd _ _ H
 #align category_theory.morphism_property.stable_under_base_change.base_change_map CategoryTheory.MorphismProperty.StableUnderBaseChange.baseChange_map
@@ -242,7 +242,7 @@ theorem StableUnderBaseChange.pullback_map [HasPullbacks C] {P : MorphismPropert
           ((baseChange _).map (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g')).left) ≫
         (pullbackSymmetry _ _).hom ≫
           ((baseChange g').map (Over.homMk _ e₁.symm : Over.mk f ⟶ Over.mk f')).left :=
-    by apply pullback.hom_ext <;> dsimp <;> simp
+    by ext <;> dsimp <;> simp
   rw [this]
   apply hP' <;> rw [hP.respectsIso.cancel_left_isIso]
   exacts [hP.baseChange_map _ (Over.homMk _ e₂.symm : Over.mk g ⟶ Over.mk g') h₂,
diff --git a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
index 301e230414b4a..5914f14423e88 100644
--- a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
@@ -214,7 +214,7 @@ theorem biproduct.total : (∑ j : J, biproduct.π f j ≫ biproduct.ι f j) = 
 
 theorem biproduct.lift_eq {T : C} {g : ∀ j, T ⟶ f j} :
     biproduct.lift g = ∑ j, g j ≫ biproduct.ι f j := by
-  apply biproduct.hom_ext; intro j
+  ext j
   simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
     Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]
 #align category_theory.limits.biproduct.lift_eq CategoryTheory.Limits.biproduct.lift_eq
@@ -280,13 +280,13 @@ def biproduct.reindex {β γ : Type} [Fintype β] [DecidableEq β] [DecidableEq
   hom := biproduct.desc fun b => biproduct.ι f (ε b)
   inv := biproduct.lift fun b => biproduct.π f (ε b)
   hom_inv_id := by
-    apply biproduct.hom_ext; intro b; apply biproduct.hom_ext'; intro b'
+    ext b b'
     by_cases h : b' = b
     · subst h; simp
     · have : ε b' ≠ ε b := by simp [h]
       simp [biproduct.ι_π_ne _ h, biproduct.ι_π_ne _ this]
   inv_hom_id := by
-    apply biproduct.hom_ext; intro g; apply biproduct.hom_ext'; intro g'
+    ext g g'
     by_cases h : g' = g <;>
       simp [Preadditive.sum_comp, Preadditive.comp_sum, biproduct.ι_π, biproduct.ι_π_assoc,
         comp_dite, Equiv.apply_eq_iff_eq_symm_apply, Finset.sum_dite_eq' Finset.univ (ε.symm g') _,
@@ -466,7 +466,7 @@ theorem biprod.lift_desc {T U : C} {f : T ⟶ X} {g : T ⟶ Y} {h : X ⟶ U} {i
 
 theorem biprod.map_eq [HasBinaryBiproducts C] {W X Y Z : C} {f : W ⟶ Y} {g : X ⟶ Z} :
     biprod.map f g = biprod.fst ≫ f ≫ biprod.inl + biprod.snd ≫ g ≫ biprod.inr := by
-  apply biprod.hom_ext <;> apply biprod.hom_ext' <;> simp
+  ext <;> simp
 #align category_theory.limits.biprod.map_eq CategoryTheory.Limits.biprod.map_eq
 
 /-- Every split mono `f` with a cokernel induces a binary bicone with `f` as its `inl` and
@@ -705,7 +705,7 @@ theorem Biprod.ofComponents_eq (f : X₁ ⊞ X₂ ⟶ Y₁ ⊞ Y₂) :
     Biprod.ofComponents (biprod.inl ≫ f ≫ biprod.fst) (biprod.inl ≫ f ≫ biprod.snd)
         (biprod.inr ≫ f ≫ biprod.fst) (biprod.inr ≫ f ≫ biprod.snd) =
       f := by
-  apply biprod.hom_ext' <;> apply biprod.hom_ext <;>
+  ext <;>
     simp only [Category.comp_id, biprod.inr_fst, biprod.inr_snd, biprod.inl_snd, add_zero, zero_add,
       Biprod.inl_ofComponents, Biprod.inr_ofComponents, eq_self_iff_true, Category.assoc,
       comp_zero, biprod.inl_fst, Preadditive.add_comp]
@@ -719,7 +719,7 @@ theorem Biprod.ofComponents_comp {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ :
       Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁)
         (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) := by
   dsimp [Biprod.ofComponents]
-  apply biprod.hom_ext <;> apply biprod.hom_ext' <;>
+  ext <;>
     simp only [add_comp, comp_add, add_comp_assoc, add_zero, zero_add, biprod.inl_fst,
       biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
       biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]
@@ -932,8 +932,8 @@ def preservesBiproductOfMonoBiproductComparison {f : J → C} [HasBiproduct f]
   have that : piComparison F f =
       (F.mapIso (biproduct.isoProduct f)).inv ≫
         biproductComparison F f ≫ (biproduct.isoProduct _).hom := by
-    apply limit.hom_ext; intro j
-    convert piComparison_comp_π F f j.as; simp [← Functor.map_comp]
+    ext j
+    convert piComparison_comp_π F f j; simp [← Functor.map_comp]
   haveI : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
   haveI : IsIso (piComparison F f) := by
     rw [that]
@@ -1048,7 +1048,7 @@ def preservesBinaryBiproductOfMonoBiprodComparison {X Y : C} [HasBinaryBiproduct
   have that :
     prodComparison F X Y =
       (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom :=
-    by apply prod.hom_ext <;> simp [← Functor.map_comp]
+    by ext <;> simp [← Functor.map_comp]
   haveI : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _
   haveI : IsIso (prodComparison F X Y) := by
     rw [that]
diff --git a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
index 04457b4de4450..769310586933d 100644
--- a/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
+++ b/Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
@@ -93,12 +93,7 @@ noncomputable def matrixDecomposition (o : HomOrthogonal s) {α β : Type} [Fint
     biproduct.matrix fun j k =>
       if h : f j = g k then z (f j) ⟨k, by simp [h]⟩ ⟨j, by simp⟩ ≫ eqToHom (by simp [h]) else 0
   left_inv z := by
-    -- Porting note: `ext j k` applies the lemmas in the other order,
-    -- and gets stuck. Consider adjusting priorities, or making this proof more robust.
-    apply biproduct.hom_ext
-    intro j
-    apply biproduct.hom_ext'
-    intro k
+    ext j k
     simp only [biproduct.matrix_π, biproduct.ι_desc]
     split_ifs with h
     · simp
diff --git a/Mathlib/CategoryTheory/Preadditive/Mat.lean b/Mathlib/CategoryTheory/Preadditive/Mat.lean
index f0872414a06da..6a510e61cd5a8 100644
--- a/Mathlib/CategoryTheory/Preadditive/Mat.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Mat.lean
@@ -119,6 +119,7 @@ instance : Category.{v₁} (Mat_ C) where
     rw [Finset.sum_comm]
 
 -- porting note: added because `DMatrix.ext` is not triggered automatically
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 theorem hom_ext {M N : Mat_ C} (f g : M ⟶ N) (H : ∀ i j, f i j = g i j) : f = g :=
   DMatrix.ext_iff.mp H
@@ -408,11 +409,11 @@ theorem additiveObjIsoBiproduct_naturality (F : Mat_ C ⥤ D) [Functor.Additive
     F.map f ≫ (additiveObjIsoBiproduct F N).hom =
       (additiveObjIsoBiproduct F M).hom ≫
         biproduct.matrix fun i j => F.map ((embedding C).map (f i j)) := by
-  refine' biproduct.hom_ext _ _ (fun i => _)
+  ext i : 1
   simp only [Category.assoc, additiveObjIsoBiproduct_hom_π, isoBiproductEmbedding_hom,
     embedding_obj_ι, embedding_obj_X, biproduct.lift_π, biproduct.matrix_π,
     ← cancel_epi (additiveObjIsoBiproduct F M).inv, Iso.inv_hom_id_assoc]
-  refine' biproduct.hom_ext' _ _ (fun j => _)
+  ext j : 1
   simp only [ι_additiveObjIsoBiproduct_inv_assoc, isoBiproductEmbedding_inv,
     biproduct.ι_desc, ← F.map_comp]
   congr 1
@@ -440,7 +441,7 @@ def lift (F : C ⥤ D) [Functor.Additive F] : Mat_ C ⥤ D where
   map_id X := by
     dsimp
     ext i j
-    by_cases h : i = j
+    by_cases h : j = i
     . subst h; simp
     . simp [h]
 set_option linter.uppercaseLean3 false in
@@ -572,6 +573,7 @@ section
 variable {R : Type u} [Semiring R]
 
 -- porting note: added because `Matrix.ext` is not triggered automatically
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 theorem hom_ext {X Y : Mat R} (f g : X ⟶ Y) (h : ∀ i j, f i j = g i j) : f = g :=
   Matrix.ext_iff.mp h
diff --git a/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean b/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
index 719459af09288..842691e11abcf 100644
--- a/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
+++ b/Mathlib/CategoryTheory/Sites/CompatiblePlus.lean
@@ -50,6 +50,7 @@ def diagramCompIso (X : C) : J.diagram P X ⋙ F ≅ J.diagram (P ⋙ F) X :=
     (by
       intro A B f
       -- porting note: this used to work with `ext`
+      -- See https://github.com/leanprover-community/mathlib4/issues/5229
       apply Multiequalizer.hom_ext
       dsimp
       simp only [Functor.mapCone_π_app, Multiequalizer.multifork_π_app_left, Iso.symm_hom,
@@ -148,6 +149,7 @@ theorem plusCompIso_whiskerLeft {F G : D ⥤ E} (η : F ⟶ G) (P : Cᵒᵖ ⥤
   simp only [← Category.assoc]
   congr 1
   -- porting note: this used to work with `ext`
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   apply Multiequalizer.hom_ext
   intro a
   dsimp
@@ -184,6 +186,7 @@ theorem plusCompIso_whiskerRight {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) :
   simp only [← Category.assoc]
   congr 1
   -- porting note: this used to work with `ext`
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   apply Multiequalizer.hom_ext
   intro a
   dsimp
@@ -209,6 +212,7 @@ theorem whiskerRight_toPlus_comp_plusCompIso_hom :
   simp only [← Category.assoc]
   congr 1
   -- porting note: this used to work with `ext`
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   apply Multiequalizer.hom_ext
   delta Cover.toMultiequalizer
   simp only [diagramCompIso_hom_ι, Category.assoc, ← F.map_comp]
diff --git a/Mathlib/CategoryTheory/Sites/CoverLifting.lean b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
index a75041e434772..153ebac79503b 100644
--- a/Mathlib/CategoryTheory/Sites/CoverLifting.lean
+++ b/Mathlib/CategoryTheory/Sites/CoverLifting.lean
@@ -258,6 +258,8 @@ set_option linter.uppercaseLean3 false in
 theorem gluedSection_isAmalgamation : x.IsAmalgamation (gluedSection hu ℱ hS hx) := by
   intro V fV hV
   -- porting note: next line was `ext W`
+  -- Now `ext` can't see that `ran` is defined as a limit.
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   refine limit.hom_ext (λ (W : StructuredArrow (op V) G.op) => ?_)
   simp only [Functor.comp_map, limit.lift_pre, coyoneda_obj_map, ran_obj_map, gluedSection]
   erw [limit.lift_π]
@@ -273,6 +275,8 @@ set_option linter.uppercaseLean3 false in
 theorem gluedSection_is_unique (y) (hy : x.IsAmalgamation y) : y = gluedSection hu ℱ hS hx := by
   unfold gluedSection limit.lift
   -- porting note: next line was `ext W`
+  -- Now `ext` can't see that `ran` is defined as a limit.
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   refine limit.hom_ext (λ (W : StructuredArrow (op U) G.op) => ?_)
   erw [limit.lift_π]
   convert helper hu ℱ hS hx (𝟙 _) y W _
diff --git a/Mathlib/CategoryTheory/Sites/Pretopology.lean b/Mathlib/CategoryTheory/Sites/Pretopology.lean
index 691c3e4bb088d..5304b34353dda 100644
--- a/Mathlib/CategoryTheory/Sites/Pretopology.lean
+++ b/Mathlib/CategoryTheory/Sites/Pretopology.lean
@@ -181,7 +181,7 @@ def trivial : Pretopology C where
     rintro ⟨Z, g, i, rfl⟩
     refine' ⟨pullback g f, pullback.snd, _, _⟩
     · refine' ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨_, by aesop_cat⟩⟩⟩
-      apply pullback.hom_ext
+      ext
       · rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
         simp
       · simp
diff --git a/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean b/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
index a667b1e56e948..555d2bf0268b2 100644
--- a/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
+++ b/Mathlib/CategoryTheory/Sites/SheafOfTypes.lean
@@ -818,13 +818,6 @@ variable (P R)
 def firstObjEqFamily : FirstObj P R ≅ R.FamilyOfElements P where
   hom t Y f hf := Pi.π (fun f : ΣY, { f : Y ⟶ X // R f } => P.obj (op f.1)) ⟨_, _, hf⟩ t
   inv := Pi.lift fun f x => x _ f.2.2
-  hom_inv_id := by
-    funext
-    ext
-    simp
-  inv_hom_id := by
-    funext
-    apply Limits.Types.Limit.lift_π_apply'
 #align category_theory.equalizer.first_obj_eq_family CategoryTheory.Equalizer.firstObjEqFamily
 
 instance : Inhabited (FirstObj P (⊥ : Presieve X)) :=
@@ -885,8 +878,7 @@ def secondMap : FirstObj P (S : Presieve X) ⟶ SecondObj P S :=
 #align category_theory.equalizer.sieve.second_map CategoryTheory.Equalizer.Sieve.secondMap
 
 theorem w : forkMap P (S : Presieve X) ≫ firstMap P S = forkMap P S ≫ secondMap P S := by
-  apply limit.hom_ext
-  rintro ⟨Y, Z, g, f, hf⟩
+  ext
   simp [firstMap, secondMap, forkMap]
 #align category_theory.equalizer.sieve.w CategoryTheory.Equalizer.Sieve.w
 
@@ -944,7 +936,7 @@ variable [HasPullbacks C]
 /-- The rightmost object of the fork diagram of https://stacks.math.columbia.edu/tag/00VM, which
 contains the data used to check a family of elements for a presieve is compatible.
 -/
-def SecondObj : Type max v₁ u₁ :=
+@[simp] def SecondObj : Type max v₁ u₁ :=
   ∏ fun fg : (ΣY, { f : Y ⟶ X // R f }) × ΣZ, { g : Z ⟶ X // R g } =>
     P.obj (op (pullback fg.1.2.1 fg.2.2.1))
 #align category_theory.equalizer.presieve.second_obj CategoryTheory.Equalizer.Presieve.SecondObj
@@ -963,8 +955,8 @@ def secondMap : FirstObj P R ⟶ SecondObj P R :=
 #align category_theory.equalizer.presieve.second_map CategoryTheory.Equalizer.Presieve.secondMap
 
 theorem w : forkMap P R ≫ firstMap P R = forkMap P R ≫ secondMap P R := by
-  apply limit.hom_ext
-  rintro ⟨⟨Y, f, hf⟩, ⟨Z, g, hg⟩⟩
+  dsimp
+  ext
   simp only [firstMap, secondMap, forkMap]
   simp only [limit.lift_π, limit.lift_π_assoc, assoc, Fan.mk_π_app]
   rw [← P.map_comp, ← op_comp, pullback.condition]
diff --git a/Mathlib/CategoryTheory/StructuredArrow.lean b/Mathlib/CategoryTheory/StructuredArrow.lean
index 5aaf29465b457..e91df8ecaa6fb 100644
--- a/Mathlib/CategoryTheory/StructuredArrow.lean
+++ b/Mathlib/CategoryTheory/StructuredArrow.lean
@@ -56,6 +56,7 @@ variable {S S' S'' : D} {Y Y' : C} {T : C ⥤ D}
 
 -- porting note: this lemma was added because `Comma.hom_ext`
 -- was not triggered automatically
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma hom_ext {X Y : StructuredArrow S T} (f g : X ⟶ Y) (h : f.right = g.right) : f = g :=
   CommaMorphism.ext _ _ (Subsingleton.elim _ _) h
@@ -289,6 +290,7 @@ variable {T T' T'' : D} {Y Y' : C} {S : C ⥤ D}
 
 -- porting note: this lemma was added because `Comma.hom_ext`
 -- was not triggered automatically
+-- See https://github.com/leanprover-community/mathlib4/issues/5229
 @[ext]
 lemma hom_ext {X Y : CostructuredArrow S T} (f g : X ⟶ Y) (h : f.left = g.left) : f = g :=
   CommaMorphism.ext _ _ h (Subsingleton.elim _ _)
@@ -448,7 +450,7 @@ instance proj_reflectsIsomorphisms : ReflectsIsomorphisms (proj S T) where
     ⟨⟨CostructuredArrow.homMk
         (inv ((proj S T).map f))
         (by rw [Functor.map_inv, IsIso.inv_comp_eq]; simp),
-      by constructor <;> apply Comma.hom_ext <;> dsimp at t ⊢ <;> simp⟩⟩
+      by constructor <;> ext <;> dsimp at t ⊢ <;> simp⟩⟩
 #align category_theory.costructured_arrow.proj_reflects_iso CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms
 
 open CategoryTheory.Limits
@@ -460,10 +462,9 @@ def mkIdTerminal [Full S] [Faithful S] : IsTerminal (mk (𝟙 (S.obj Y))) where
   lift c := homMk (S.preimage c.pt.hom)
   uniq := by
     rintro c m -
-    apply CommaMorphism.ext
-    · apply S.map_injective
-      simpa only [homMk_left, S.image_preimage, ← w m] using (Category.comp_id _).symm
-    · aesop_cat
+    ext
+    apply S.map_injective
+    simpa only [homMk_left, S.image_preimage, ← w m] using (Category.comp_id _).symm
 #align category_theory.costructured_arrow.mk_id_terminal CategoryTheory.CostructuredArrow.mkIdTerminal
 
 variable {A : Type u₃} [Category.{v₃} A] {B : Type u₄} [Category.{v₄} B]
diff --git a/Mathlib/CategoryTheory/Subobject/Lattice.lean b/Mathlib/CategoryTheory/Subobject/Lattice.lean
index ce7bf2880c43a..c7c5d111a0463 100644
--- a/Mathlib/CategoryTheory/Subobject/Lattice.lean
+++ b/Mathlib/CategoryTheory/Subobject/Lattice.lean
@@ -205,7 +205,7 @@ def supLe {A : C} (f g h : MonoOver A) : (f ⟶ h) → (g ⟶ h) → ((sup.obj f
   intro k₁ k₂
   refine' homMk _ _
   apply image.lift ⟨_, h.arrow, coprod.desc k₁.left k₂.left, _⟩
-  . apply coprod.hom_ext
+  . ext
     · simp [w k₁]
     · simp [w k₂]
   · apply image.lift_fac
diff --git a/Mathlib/Topology/Sheaves/Forget.lean b/Mathlib/Topology/Sheaves/Forget.lean
index b0441bc7a43e9..b26b0a070b256 100644
--- a/Mathlib/Topology/Sheaves/Forget.lean
+++ b/Mathlib/Topology/Sheaves/Forget.lean
@@ -72,22 +72,26 @@ def diagramCompPreservesLimits : diagram F U ⋙ G ≅ diagram.{v} (F ⋙ G) U :
   exact PreservesProduct.iso _ _
   exact PreservesProduct.iso _ _
   rintro ⟨⟩ ⟨⟩ ⟨⟩
-  · -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext (fun j => ?_)
     simp
-  · -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext (fun j => ?_)
     -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
     dsimp [diagram, leftRes, rightRes]
     simp [limit.lift_π, Functor.comp_map, map_lift_piComparison, Fan.mk_π_app,
       PreservesProduct.iso_hom, parallelPair_map_left, Functor.map_comp, Category.assoc]
-  · -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext (fun j => ?_)
     -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
     dsimp [diagram, leftRes, rightRes]
     simp [limit.lift_π, Functor.comp_map, map_lift_piComparison, Fan.mk_π_app,
       PreservesProduct.iso_hom, parallelPair_map_left, Functor.map_comp, Category.assoc]
-  · -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext (fun j => ?_)
     simp [diagram, leftRes, rightRes]
 set_option linter.uppercaseLean3 false in
@@ -105,12 +109,14 @@ def mapConeFork :
   Cones.ext (Iso.refl _) fun j => by
     dsimp; simp [diagramCompPreservesLimits]; cases j <;> dsimp
     · rw [Iso.eq_comp_inv]
-      -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+      -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+      -- See https://github.com/leanprover-community/mathlib4/issues/5229
       refine limit.hom_ext (fun j => ?_)
       -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
       simp [diagram, leftRes, rightRes, res]
     · rw [Iso.eq_comp_inv]
-      -- Porting note : can't use `limit.hom_ext` as an `ext` lemma
+      -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+      -- See https://github.com/leanprover-community/mathlib4/issues/5229
       refine limit.hom_ext (fun j => ?_)
       -- Porting note : `attribute [local reducible]` doesn't work, this is its replacement
       dsimp [diagram, leftRes, rightRes, res]
@@ -211,6 +217,8 @@ theorem isSheaf_iff_isSheaf_comp : Presheaf.IsSheaf F ↔ Presheaf.IsSheaf (F 
       let f' : c ⟶ d' := Fork.mkHom (G.map f) (by
         dsimp only [diagramCompPreservesLimits, res]
         dsimp only [Fork.ι]
+        -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+        -- See https://github.com/leanprover-community/mathlib4/issues/5229
         refine limit.hom_ext fun j => ?_
         dsimp
         simp only [Category.assoc, ← Functor.map_comp_assoc, equalizer.lift_ι,
diff --git a/Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean b/Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
index 81fbd6e1c7020..1eb800b49fb8e 100644
--- a/Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
+++ b/Mathlib/Topology/Sheaves/SheafCondition/EqualizerProducts.lean
@@ -89,7 +89,8 @@ set_option linter.uppercaseLean3 false in
 @[elementwise]
 theorem w : res F U ≫ leftRes F U = res F U ≫ rightRes F U := by
   dsimp [res, leftRes, rightRes]
-  -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+  -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+  -- See https://github.com/leanprover-community/mathlib4/issues/5229
   refine limit.hom_ext (fun _ => ?_)
   simp only [limit.lift_π, limit.lift_π_assoc, Fan.mk_π_app, Category.assoc]
   rw [← F.map_comp]
@@ -162,13 +163,15 @@ def diagram.isoOfIso (α : F ≅ G) : diagram F U ≅ diagram.{v'} G U :=
     (by
       rintro ⟨⟩ ⟨⟩ ⟨⟩
       · simp
-      · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+      · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+        -- See https://github.com/leanprover-community/mathlib4/issues/5229
         refine limit.hom_ext (fun _ => ?_)
         simp only [leftRes, piOpens.isoOfIso, piInters.isoOfIso, parallelPair_map_left,
           Functor.mapIso_hom, lim_map, limit.lift_map, limit.lift_π, Cones.postcompose_obj_π,
           NatTrans.comp_app, Fan.mk_π_app, Discrete.natIso_hom_app, Iso.app_hom, Category.assoc,
           NatTrans.naturality, limMap_π_assoc]
-      · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+      · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+        -- See https://github.com/leanprover-community/mathlib4/issues/5229
         refine limit.hom_ext (fun _ => ?_)
         simp only [rightRes, piOpens.isoOfIso, piInters.isoOfIso, parallelPair_map_right,
           Functor.mapIso_hom, lim_map, limit.lift_map, limit.lift_π, Cones.postcompose_obj_π,
@@ -187,7 +190,8 @@ def fork.isoOfIso (α : F ≅ G) :
     fork F U ≅ (Cones.postcompose (diagram.isoOfIso U α).inv).obj (fork G U) := by
   fapply Fork.ext
   · apply α.app
-  · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext (fun _ => ?_)
     dsimp only [Fork.ι]
     -- Ugh, `simp` can't unfold abbreviations.
@@ -231,14 +235,16 @@ def coneEquivFunctorObj (c : Cone ((diagram U).op ⋙ F)) :
           (Pi.lift fun b : ι × ι => c.π.app (op (pair b.1 b.2)))
       naturality := fun Y Z f => by
         cases Y <;> cases Z <;> cases f
-        · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+        · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+          -- See https://github.com/leanprover-community/mathlib4/issues/5229
           refine limit.hom_ext fun i => ?_
           dsimp
           simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app, CategoryTheory.Functor.map_id,
             Category.assoc]
           dsimp
           simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app]
-        · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+        · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+          -- See https://github.com/leanprover-community/mathlib4/issues/5229
           refine limit.hom_ext fun ⟨i, j⟩ => ?_
           dsimp [SheafConditionEqualizerProducts.leftRes]
           simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
@@ -246,7 +252,8 @@ def coneEquivFunctorObj (c : Cone ((diagram U).op ⋙ F)) :
           have h := c.π.naturality (Quiver.Hom.op (Hom.left i j))
           dsimp at h
           simpa using h
-        · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+        · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+          -- See https://github.com/leanprover-community/mathlib4/issues/5229
           refine limit.hom_ext fun ⟨i, j⟩ => ?_
           dsimp [SheafConditionEqualizerProducts.rightRes]
           simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
@@ -254,7 +261,8 @@ def coneEquivFunctorObj (c : Cone ((diagram U).op ⋙ F)) :
           have h := c.π.naturality (Quiver.Hom.op (Hom.right i j))
           dsimp at h
           simpa using h
-        · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+        · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+          -- See https://github.com/leanprover-community/mathlib4/issues/5229
           refine limit.hom_ext fun i => ?_
           dsimp
           simp only [limit.lift_π, Category.id_comp, Fan.mk_π_app, CategoryTheory.Functor.map_id,
@@ -276,7 +284,9 @@ def coneEquivFunctor :
     { Hom := f.Hom
       w := fun j => by
         cases j <;>
-          · refine limit.hom_ext fun i => ?_
+          · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+            -- See https://github.com/leanprover-community/mathlib4/issues/5229
+            refine limit.hom_ext fun i => ?_
             simp only [Limits.Fan.mk_π_app, Limits.ConeMorphism.w, Limits.limit.lift_π,
               Category.assoc, coneEquivFunctorObj_π_app] }
 set_option linter.uppercaseLean3 false in
@@ -371,12 +381,6 @@ def coneEquivUnitIsoApp (c : Cone ((diagram U).op ⋙ F)) :
         rcases j with ⟨⟩ <;>
         · dsimp [coneEquivInverse]
           simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] }
-  hom_inv_id := by
-    ext
-    simp only [Category.comp_id, (. ≫ .), (𝟙 .)]
-  inv_hom_id := by
-    ext
-    simp only [Category.comp_id, (. ≫ .), (𝟙 .)]
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.sheaf_condition_pairwise_intersections.cone_equiv_unit_iso_app TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivUnitIsoApp
 
@@ -399,11 +403,13 @@ def coneEquivCounitIso :
           { Hom := 𝟙 _
             w := by
               rintro ⟨_ | _⟩
-              · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+              · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+                -- See https://github.com/leanprover-community/mathlib4/issues/5229
                 refine limit.hom_ext fun ⟨j⟩ => ?_
                 dsimp [coneEquivInverse]
                 simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
-              · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+              · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+                -- See https://github.com/leanprover-community/mathlib4/issues/5229
                 refine limit.hom_ext fun ⟨i, j⟩ => ?_
                 dsimp [coneEquivInverse]
                 simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] }
@@ -411,22 +417,16 @@ def coneEquivCounitIso :
           { Hom := 𝟙 _
             w := by
               rintro ⟨_ | _⟩
-              · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+              · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+                -- See https://github.com/leanprover-community/mathlib4/issues/5229
                 refine limit.hom_ext fun ⟨j⟩ => ?_
                 dsimp [coneEquivInverse]
                 simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π]
-              · -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+              · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+                -- See https://github.com/leanprover-community/mathlib4/issues/5229
                 refine limit.hom_ext fun ⟨i, j⟩ => ?_
                 dsimp [coneEquivInverse]
-                simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] }
-        hom_inv_id := by
-          ext
-          dsimp
-          simp only [Category.comp_id]
-        inv_hom_id := by
-          ext
-          dsimp
-          simp only [Category.comp_id] })
+                simp only [Limits.Fan.mk_π_app, Category.id_comp, Limits.limit.lift_π] } })
     fun {c d} f => by
     ext
     dsimp
@@ -462,10 +462,9 @@ def isLimitMapConeOfIsLimitSheafConditionFork
         { Hom := 𝟙 _
           w := by
             intro x
-            induction x using Opposite.rec' with | h x => ?_
+            induction x with | h x => ?_
             rcases x with ⟨⟩
-            · dsimp
-              simp
+            · simp
               rfl
             · dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                 SheafConditionEqualizerProducts.leftRes]
@@ -477,25 +476,16 @@ def isLimitMapConeOfIsLimitSheafConditionFork
         { Hom := 𝟙 _
           w := by
             intro x
-            induction x using Opposite.rec' with | h x => ?_
+            induction x with | h x => ?_
             rcases x with ⟨⟩
-            · dsimp
-              simp
+            · simp
               rfl
             · dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                 SheafConditionEqualizerProducts.leftRes]
               simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                 Category.assoc]
               rw [← F.map_comp]
-              rfl }
-      hom_inv_id := by
-        ext
-        dsimp
-        simp only [Category.comp_id]
-      inv_hom_id := by
-        ext
-        dsimp
-        simp only [Category.comp_id] }
+              rfl } }
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_map_cone_of_is_limit_sheaf_condition_fork TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitMapConeOfIsLimitSheafConditionFork
 
@@ -509,11 +499,10 @@ def isLimitSheafConditionForkOfIsLimitMapCone (Q : IsLimit (F.mapCone (cocone U)
         { Hom := 𝟙 _
           w := by
             rintro ⟨⟩
-            · dsimp
-              simp
+            · simp
               rfl
-            · dsimp
-              -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+            · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+              -- See https://github.com/leanprover-community/mathlib4/issues/5229
               refine limit.hom_ext fun ⟨i, j⟩ => ?_
               dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                 SheafConditionEqualizerProducts.leftRes]
@@ -525,26 +514,17 @@ def isLimitSheafConditionForkOfIsLimitMapCone (Q : IsLimit (F.mapCone (cocone U)
         { Hom := 𝟙 _
           w := by
             rintro ⟨⟩
-            · dsimp
-              simp
+            · simp
               rfl
-            · dsimp
-              -- Porting note : Lean can't use `limit.hom_ext` as `ext` lemma
+            · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+              -- See https://github.com/leanprover-community/mathlib4/issues/5229
               refine limit.hom_ext fun ⟨i, j⟩ => ?_
               dsimp [coneEquivInverse, SheafConditionEqualizerProducts.res,
                 SheafConditionEqualizerProducts.leftRes]
               simp only [limit.lift_π, limit.lift_π_assoc, Category.id_comp, Fan.mk_π_app,
                 Category.assoc]
               rw [← F.map_comp]
-              rfl }
-      hom_inv_id := by
-        ext
-        dsimp
-        simp only [Category.comp_id]
-      inv_hom_id := by
-        ext
-        dsimp
-        simp only [Category.comp_id] }
+              rfl } }
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.sheaf_condition_pairwise_intersections.is_limit_sheaf_condition_fork_of_is_limit_map_cone TopCat.Presheaf.SheafConditionPairwiseIntersections.isLimitSheafConditionForkOfIsLimitMapCone
 
diff --git a/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean b/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
index 2fb646f5b89e5..c1abde226e69c 100644
--- a/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
+++ b/Mathlib/Topology/Sheaves/SheafCondition/UniqueGluing.lean
@@ -160,7 +160,8 @@ theorem isSheaf_of_isSheafUniqueGluing_types (Fsh : F.IsSheafUniqueGluing) : F.I
   choose m m_spec m_uniq using fun x : s.pt =>
     Fsh U ((piOpensIsoSectionsFamily F U).hom (s.ι x)) (h_compatible x)
   refine' ⟨m, _, _⟩
-  · -- Porting note : Lean can't use `limit.hom_ext` as an `ext` lemma
+  · -- Porting note : `ext` can't see `limit.hom_ext` applies here:
+    -- See https://github.com/leanprover-community/mathlib4/issues/5229
     refine limit.hom_ext fun ⟨i⟩ => funext fun x => ?_
     simp [res]
     exact m_spec x i
diff --git a/Mathlib/Topology/Sheaves/Stalks.lean b/Mathlib/Topology/Sheaves/Stalks.lean
index 535ed2d6c24b6..5c06bf87aaaf9 100644
--- a/Mathlib/Topology/Sheaves/Stalks.lean
+++ b/Mathlib/Topology/Sheaves/Stalks.lean
@@ -122,6 +122,7 @@ set_option linter.uppercaseLean3 false in
 /-- A morphism from the stalk of `F` at `x` to some object `Y` is completely determined by its
 composition with the `germ` morphisms.
 -/
+@[ext]
 theorem stalk_hom_ext (F : X.Presheaf C) {x} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y}
     (ih : ∀ (U : Opens X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂) : f₁ = f₂ :=
   colimit.hom_ext fun U => by
@@ -342,16 +343,18 @@ set_option linter.uppercaseLean3 false in
 
 @[simp]
 theorem stalkSpecializes_refl {C : Type _} [Category C] [Limits.HasColimits C] {X : TopCat}
-    (F : X.Presheaf C) (x : X) : F.stalkSpecializes (specializes_refl x) = 𝟙 _ :=
-  F.stalk_hom_ext fun _ _ => by dsimp; simp
+    (F : X.Presheaf C) (x : X) : F.stalkSpecializes (specializes_refl x) = 𝟙 _ := by
+  ext
+  simp
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.stalk_specializes_refl TopCat.Presheaf.stalkSpecializes_refl
 
 @[reassoc (attr := simp), elementwise (attr := simp)]
 theorem stalkSpecializes_comp {C : Type _} [Category C] [Limits.HasColimits C] {X : TopCat}
     (F : X.Presheaf C) {x y z : X} (h : x ⤳ y) (h' : y ⤳ z) :
-    F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h') :=
-  F.stalk_hom_ext fun _ _ => by simp
+    F.stalkSpecializes h' ≫ F.stalkSpecializes h = F.stalkSpecializes (h.trans h') := by
+  ext
+  simp
 set_option linter.uppercaseLean3 false in
 #align Top.presheaf.stalk_specializes_comp TopCat.Presheaf.stalkSpecializes_comp