diff --git a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
index 694fe45fcdcccc..f074a92e287903 100644
--- a/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
+++ b/Mathlib/AlgebraicGeometry/IdealSheaf/Subscheme.lean
@@ -715,6 +715,7 @@ open IdealSheafData in
 noncomputable
 def kerAdjunction (Y : Scheme.{u}) : (subschemeFunctor Y).rightOp ⊣ Y.kerFunctor where
   unit.app I := eqToHom (by simp)
+  unit.naturality _ _ _ := rfl
   counit.app f := (Over.homMk f.unop.hom.toImage f.unop.hom.toImage_imageι).op
   counit.naturality _ _ _ := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
   left_triangle_components I := Quiver.Hom.unop_inj (by ext1; simp [← cancel_mono (subschemeι _)])
diff --git a/Mathlib/CategoryTheory/Category/Basic.lean b/Mathlib/CategoryTheory/Category/Basic.lean
index ac969b751ae7fb..28d4524d7a65f3 100644
--- a/Mathlib/CategoryTheory/Category/Basic.lean
+++ b/Mathlib/CategoryTheory/Category/Basic.lean
@@ -107,27 +107,6 @@ open Lean Meta Elab.Tactic in
   else
     throwError "The goal does not contain `sorry`"
 
-/--
-`rfl_cat` is a macro for `intros; rfl` which is attempted in `aesop_cat` before
-doing the more expensive `aesop` tactic.
-
-This gives a speedup because `simp` (called by `aesop`) is too slow.
-There is a fix for this slowness in https://github.com/leanprover/lean4/pull/7428.
-So, when that is resolved, the performance impact of `rfl_cat` should be measured again.
-
-Implementation notes:
-* `refine id ?_`:
-  In some cases it is important that the type of the proof matches the expected type exactly.
-  e.g. if the goal is `2 = 1 + 1`, the `rfl` tactic will give a proof of type `2 = 2`.
-  Starting a proof with `refine id ?_` is a trick to make sure that the proof has exactly
-  the expected type, in this case `2 = 1 + 1`. See also https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/changing.20a.20proof.20can.20break.20a.20later.20proof
-* `apply_rfl`:
-  `rfl` is a macro that attempts both `eq_refl` and `apply_rfl`. Since `apply_rfl`
-  subsumes `eq_refl`, we can use `apply_rfl` instead. This fails twice as fast as `rfl`.
-
--/
-macro (name := rfl_cat) "rfl_cat" : tactic => do `(tactic| (refine id ?_; intros; apply_rfl))
-
 /--
 A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and
 allows `aesop` to look through semireducible definitions when calling `intros`.
@@ -136,7 +115,7 @@ use in auto-params.
 -/
 macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  first | sorry_if_sorry | rfl_cat |
+  first | sorry_if_sorry |
   aesop $c* (config := { introsTransparency? := some .default, terminal := true })
             (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 
@@ -145,7 +124,7 @@ We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop
 -/
 macro (name := aesop_cat?) "aesop_cat?" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  first | sorry_if_sorry | try_this rfl_cat |
+  first | sorry_if_sorry |
   aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
              (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 /--
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
index 35590897d96442..86973f560edf90 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
@@ -176,7 +176,8 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgCat R where
                 ext : 1
                 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
                 refine TensorProduct.ext ?_
-                rfl }
+                rfl
+              one_hom := by rfl } -- simp fails with an error "maximum recursion depth reached"
           inv :=
             { hom := ofHom
                 { toFun := _root_.id
@@ -186,7 +187,8 @@ def monModuleEquivalenceAlgebra : Mon_ (ModuleCat.{u} R) ≌ AlgCat R where
                 ext : 1
                 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` did not pick up `TensorProduct.ext`
                 refine TensorProduct.ext ?_
-                rfl } })
+                rfl
+              one_hom := by rfl } }) -- simp fails with an error "maximum recursion depth reached"
   counitIso :=
     NatIso.ofComponents
       (fun A =>