perf(CategoryTheory): let aesop_cat attempt rfl before aesop

Mathlib/Algebra/Homology/DifferentialObject.lean

@@ -89,8 +89,6 @@ def dgoToHomologicalComplex :
         -- Porting note: this `rw` used to be part of the `simp`.
         have : f.f i ≫ Y.d i = X.d i ≫ f.f _ := (congr_fun f.comm i).symm
         rw [reassoc_of% this] }
-  map_id _ := rfl -- the `aesop_cat` autoparam solves this but it's slow
-  map_comp _ _ := rfl -- the `aesop_cat` autoparam solves this but it's slow
 
 /-- The functor from homological complexes to differential graded objects.
 -/

Mathlib/CategoryTheory/Category/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Combinatorics.Quiver.Basic
 import Mathlib.Tactic.PPWithUniv
 import Mathlib.Tactic.Common
 import Mathlib.Tactic.StacksAttribute
+import Mathlib.Tactic.TryThis
 
 /-!
 # Categories
@@ -108,6 +109,18 @@ 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.
+
+Note on `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`.
+-/
+macro (name := rfl_cat) "rfl_cat" : tactic => do `(tactic| (refine id ?_; intros; rfl))
+
 /--
 A thin wrapper for `aesop` which adds the `CategoryTheory` rule set and
 allows `aesop` to look through semireducible definitions when calling `intros`.
@@ -116,7 +129,7 @@ use in auto-params.
 -/
 macro (name := aesop_cat) "aesop_cat" c:Aesop.tactic_clause* : tactic =>
 `(tactic|
-  first | sorry_if_sorry |
+  first | sorry_if_sorry | rfl_cat |
   aesop $c* (config := { introsTransparency? := some .default, terminal := true })
             (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 
@@ -125,7 +138,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 |
+  first | sorry_if_sorry | try_this rfl_cat |
   aesop? $c* (config := { introsTransparency? := some .default, terminal := true })
              (rule_sets := [$(Lean.mkIdent `CategoryTheory):ident]))
 /--

Mathlib/CategoryTheory/DiscreteCategory.lean

@@ -167,9 +167,9 @@ theorem functor_obj {I : Type u₁} (F : I → C) (i : I) :
     (Discrete.functor F).obj (Discrete.mk i) = F i :=
   rfl
 
-@[simp]
 theorem functor_map {I : Type u₁} (F : I → C) {i : Discrete I} (f : i ⟶ i) :
     (Discrete.functor F).map f = 𝟙 (F i.as) := by aesop_cat
+
 @[simp]
 theorem functor_obj_eq_as {I : Type u₁} (F : I → C) (X : Discrete I) :
     (Discrete.functor F).obj X = F X.as :=

Mathlib/CategoryTheory/Monoidal/Mod_.lean

@@ -122,8 +122,6 @@ def comap {A B : Mon_ C} (f : A ⟶ B) : Mod_ B ⥤ Mod_ A where
         slice_rhs 1 2 => rw [whisker_exchange]
         slice_rhs 2 3 => rw [← g.act_hom]
         rw [Category.assoc] }
-  map_id _ := rfl -- the `aesop_cat` autoparam solves this but it's slow
-  map_comp _ _ := rfl -- the `aesop_cat` autoparam solves this but it's slow
 
 -- Lots more could be said about `comap`, e.g. how it interacts with
 -- identities, compositions, and equalities of monoid object morphisms.

Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean

@@ -107,7 +107,7 @@ variable {Y : Opens X}
     in the sieve. This full subcategory is equivalent to `OpensLeCover U`, the (poset)
     category of opens contained in some `U i`. -/
 @[simps]
-def generateEquivalenceOpensLe_functor' (hY : Y = iSup U) :
+def generateEquivalenceOpensLe_functor' :
     (FullSubcategory fun f : Over Y => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) ⥤
     OpensLeCover U :=
 { obj := fun f =>
@@ -150,7 +150,7 @@ def generateEquivalenceOpensLe (hY : Y = iSup U) :
     (FullSubcategory fun f : Over Y => (Sieve.generate (presieveOfCoveringAux U Y)).arrows f.hom) ≌
     OpensLeCover U where
   -- Porting note: split it out to prevent timeout
-  functor := generateEquivalenceOpensLe_functor' _ hY
+  functor := generateEquivalenceOpensLe_functor' _
   inverse := generateEquivalenceOpensLe_inverse' _ hY
   unitIso := eqToIso <| CategoryTheory.Functor.ext
     (by rintro ⟨⟨_, _⟩, _⟩; dsimp; congr)