chore: review of automation in category theory (leanprover-community#…

…4793)

Clean up of automation in the category theory library. Leaving out unnecessary proof steps, or fields done by `aesop_cat`, and making more use of available autoparameters.



Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Mathlib/Algebra/Category/GroupCat/EquivalenceGroupAddGroup.lean

@@ -85,20 +85,15 @@ end AddCommGroupCat
 @[simps!]
 def groupAddGroupEquivalence : GroupCat ≌ AddGroupCat :=
   CategoryTheory.Equivalence.mk GroupCat.toAddGroupCat AddGroupCat.toGroupCat
-    (NatIso.ofComponents (fun X => MulEquiv.toGroupCatIso (MulEquiv.multiplicativeAdditive X))
-      fun _ => rfl)
-    (NatIso.ofComponents (fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X))
-      fun _ => rfl)
+    (NatIso.ofComponents fun X => MulEquiv.toGroupCatIso (MulEquiv.multiplicativeAdditive X))
+    (NatIso.ofComponents fun X => AddEquiv.toAddGroupCatIso (AddEquiv.additiveMultiplicative X))
 #align Group_AddGroup_equivalence groupAddGroupEquivalence
 
 /-- The equivalence of categories between `CommGroup` and `AddCommGroup`.
 -/
 @[simps!]
 def commGroupAddCommGroupEquivalence : CommGroupCat ≌ AddCommGroupCat :=
   CategoryTheory.Equivalence.mk CommGroupCat.toAddCommGroupCat AddCommGroupCat.toCommGroupCat
-    (NatIso.ofComponents (fun X => MulEquiv.toCommGroupCatIso (MulEquiv.multiplicativeAdditive X))
-      fun _ => rfl)
-    (NatIso.ofComponents
-      (fun X => AddEquiv.toAddCommGroupCatIso (AddEquiv.additiveMultiplicative X)) fun _ => rfl)
+    (NatIso.ofComponents fun X => MulEquiv.toCommGroupCatIso (MulEquiv.multiplicativeAdditive X))
+    (NatIso.ofComponents fun X => AddEquiv.toAddCommGroupCatIso (AddEquiv.additiveMultiplicative X))
 #align CommGroup_AddCommGroup_equivalence commGroupAddCommGroupEquivalence
-

Mathlib/Algebra/Category/GroupCat/Limits.lean

@@ -471,7 +471,7 @@ agrees with the `subtype` map.
 @[simps! hom_left_apply_coe inv_left_apply]
 def kernelIsoKerOver {G H : AddCommGroupCat.{u}} (f : G ⟶ H) :
     Over.mk (kernel.ι f) ≅ @Over.mk _ _ G (AddCommGroupCat.of f.ker) (AddSubgroup.subtype f.ker) :=
-  Over.isoMk (kernelIsoKer f) <| by simp
+  Over.isoMk (kernelIsoKer f)
 set_option linter.uppercaseLean3 false in
 #align AddCommGroup.kernel_iso_ker_over AddCommGroupCat.kernelIsoKerOver
 

Mathlib/Algebra/Category/ModuleCat/Adjunctions.lean

@@ -391,7 +391,7 @@ instance lift_linear (F : C ⥤ D) : (lift R F).Linear R where
 is isomorphic to the original functor.
 -/
 def embeddingLiftIso (F : C ⥤ D) : embedding R C ⋙ lift R F ≅ F :=
-  NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat)
+  NatIso.ofComponents fun X => Iso.refl _
 #align category_theory.Free.embedding_lift_iso CategoryTheory.Free.embeddingLiftIso
 
 /-- Two `R`-linear functors out of the `R`-linear completion are isomorphic iff their

Mathlib/Algebra/Homology/Additive.lean

@@ -176,8 +176,7 @@ isomorphic to the identity functor. -/
 @[simps!]
 def Functor.mapHomologicalComplexIdIso (c : ComplexShape ι) :
     (𝟭 V).mapHomologicalComplex c ≅ 𝟭 _ :=
-  NatIso.ofComponents (fun K => Hom.isoOfComponents (fun i => Iso.refl _)
-    (by aesop_cat)) (by aesop_cat)
+  NatIso.ofComponents fun K => Hom.isoOfComponents fun i => Iso.refl _
 #align category_theory.functor.map_homological_complex_id_iso CategoryTheory.Functor.mapHomologicalComplexIdIso
 
 variable {V}

Mathlib/Algebra/Homology/HomologicalComplex.lean

@@ -305,7 +305,7 @@ def forget : HomologicalComplex V c ⥤ GradedObject ι V where
 just picking out the `i`-th object. -/
 @[simps!]
 def forgetEval (i : ι) : forget V c ⋙ GradedObject.eval i ≅ eval V c i :=
-  NatIso.ofComponents (fun X => Iso.refl _) (by aesop_cat)
+  NatIso.ofComponents fun X => Iso.refl _
 #align homological_complex.forget_eval HomologicalComplex.forgetEval
 
 end
@@ -484,7 +484,8 @@ def isoApp (f : C₁ ≅ C₂) (i : ι) : C₁.X i ≅ C₂.X i :=
 which commute with the differentials. -/
 @[simps]
 def isoOfComponents (f : ∀ i, C₁.X i ≅ C₂.X i)
-    (hf : ∀ i j, c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom) : C₁ ≅ C₂ where
+    (hf : ∀ i j, c.Rel i j → (f i).hom ≫ C₂.d i j = C₁.d i j ≫ (f j).hom := by aesop_cat) :
+    C₁ ≅ C₂ where
   hom :=
     { f := fun i => (f i).hom
       comm' := hf }
@@ -512,8 +513,7 @@ theorem isoOfComponents_app (f : ∀ i, C₁.X i ≅ C₂.X i)
 #align homological_complex.hom.iso_of_components_app HomologicalComplex.Hom.isoOfComponents_app
 
 theorem isIso_of_components (f : C₁ ⟶ C₂) [∀ n : ι, IsIso (f.f n)] : IsIso f :=
-  IsIso.of_iso (HomologicalComplex.Hom.isoOfComponents (fun n => asIso (f.f n))
-    (by aesop_cat))
+  IsIso.of_iso (HomologicalComplex.Hom.isoOfComponents fun n => asIso (f.f n))
 #align homological_complex.hom.is_iso_of_components HomologicalComplex.Hom.isIso_of_components
 
 /-! Lemmas relating chain maps and `dTo`/`dFrom`. -/

Mathlib/Algebra/Homology/Opposite.lean

@@ -175,11 +175,7 @@ def opUnitIso : 𝟭 (HomologicalComplex V c)ᵒᵖ ≅ opFunctor V c ⋙ opInve
 /-- Auxiliary definition for `opEquivalence`. -/
 def opCounitIso : opInverse V c ⋙ opFunctor V c ≅ 𝟭 (HomologicalComplex Vᵒᵖ c.symm) :=
   NatIso.ofComponents
-    (fun X => HomologicalComplex.Hom.isoOfComponents (fun i => Iso.refl _) fun i j _ => by simp)
-    (by
-      intro X Y f
-      ext
-      simp)
+    fun X => HomologicalComplex.Hom.isoOfComponents fun i => Iso.refl _
 #align homological_complex.op_counit_iso HomologicalComplex.opCounitIso
 
 /-- Given a category of complexes with objects in `V`, there is a natural equivalence between its
@@ -235,11 +231,7 @@ def unopUnitIso : 𝟭 (HomologicalComplex Vᵒᵖ c)ᵒᵖ ≅ unopFunctor V c
 /-- Auxiliary definition for `unopEquivalence`. -/
 def unopCounitIso : unopInverse V c ⋙ unopFunctor V c ≅ 𝟭 (HomologicalComplex V c.symm) :=
   NatIso.ofComponents
-    (fun X => HomologicalComplex.Hom.isoOfComponents (fun i => Iso.refl _) fun i j _ => by simp)
-    (by
-      intro X Y f
-      ext
-      simp)
+    fun X => HomologicalComplex.Hom.isoOfComponents fun i => Iso.refl _
 #align homological_complex.unop_counit_iso HomologicalComplex.unopCounitIso
 
 /-- Given a category of complexes with objects in `Vᵒᵖ`, there is a natural equivalence between its

Mathlib/Algebra/Homology/ShortComplex/Basic.lean

@@ -208,7 +208,8 @@ def _root_.CategoryTheory.Functor.mapShortComplex (F : C ⥤ D) [F.PreservesZero
 /-- A constructor for isomorphisms in the category `ShortComplex C`-/
 @[simps]
 def isoMk (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e₃ : S₁.X₃ ≅ S₂.X₃)
-    (comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom) (comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom) :
+    (comm₁₂ : e₁.hom ≫ S₂.f = S₁.f ≫ e₂.hom := by aesop_cat)
+    (comm₂₃ : e₂.hom ≫ S₂.g = S₁.g ≫ e₃.hom := by aesop_cat) :
     S₁ ≅ S₂ where
   hom := ⟨e₁.hom, e₂.hom, e₃.hom, comm₁₂, comm₂₃⟩
   inv := homMk e₁.inv e₂.inv e₃.inv
@@ -218,7 +219,7 @@ def isoMk (e₁ : S₁.X₁ ≅ S₂.X₁) (e₂ : S₁.X₂ ≅ S₂.X₂) (e
           ← comm₂₃, e₂.inv_hom_id_assoc])
 
 lemma isIso_of_isIso (f : S₁ ⟶ S₂) [IsIso f.τ₁] [IsIso f.τ₂] [IsIso f.τ₃] : IsIso f :=
-  IsIso.of_iso (isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃) (by aesop_cat) (by aesop_cat))
+  IsIso.of_iso (isoMk (asIso f.τ₁) (asIso f.τ₂) (asIso f.τ₃))
 
 /-- The opposite `ShortComplex` in `Cᵒᵖ` associated to a short complex in `C`. -/
 @[simps]

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -148,7 +148,7 @@ def ofIsColimitCokernelCofork (hg : S.g = 0) (c : CokernelCofork S.f) (hc : IsCo
   wi := by rw [id_comp, hg]
   hi := KernelFork.IsLimit.ofId _ hg
   wπ := CokernelCofork.condition _
-  hπ := IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by aesop_cat))
+  hπ := IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _))
 
 @[simp] lemma ofIsColimitCokernelCofork_f' (hg : S.g = 0) (c : CokernelCofork S.f)
     (hc : IsColimit c) : (ofIsColimitCokernelCofork S hg c hc).f' = S.f := by
@@ -173,7 +173,7 @@ def ofIsLimitKernelFork (hf : S.f = 0) (c : KernelFork S.g) (hc : IsLimit c) :
   i := c.ι
   π := 𝟙 _
   wi := KernelFork.condition _
-  hi := IsLimit.ofIsoLimit hc (Fork.ext (Iso.refl _) (by aesop_cat))
+  hi := IsLimit.ofIsoLimit hc (Fork.ext (Iso.refl _))
   wπ := Fork.IsLimit.hom_ext hc (by
     dsimp
     simp only [comp_id, zero_comp, Fork.IsLimit.lift_ι, Fork.ι_ofι, hf])

Mathlib/Algebra/Homology/ShortExact/Abelian.lean

@@ -33,8 +33,9 @@ variable [Abelian 𝒜]
 open ZeroObject
 
 theorem isIso_of_shortExact_of_isIso_of_isIso (h : ShortExact f g) (h' : ShortExact f' g')
-    (i₁ : A ⟶ A') (i₂ : B ⟶ B') (i₃ : C ⟶ C') (comm₁ : i₁ ≫ f' = f ≫ i₂)
-    (comm₂ : i₂ ≫ g' = g ≫ i₃) [IsIso i₁] [IsIso i₃] : IsIso i₂ := by
+    (i₁ : A ⟶ A') (i₂ : B ⟶ B') (i₃ : C ⟶ C')
+    (comm₁ : i₁ ≫ f' = f ≫ i₂ := by aesop_cat)
+    (comm₂ : i₂ ≫ g' = g ≫ i₃ := by aesop_cat) [IsIso i₁] [IsIso i₃] : IsIso i₂ := by
   obtain ⟨_⟩ := h
   obtain ⟨_⟩ := h'
   refine @Abelian.isIso_of_isIso_of_isIso_of_isIso_of_isIso 𝒜 _ _ 0 _ _ _ 0 _ _ _ 0 f g 0 f' g'
@@ -53,8 +54,7 @@ together with proofs that `f` is mono and `g` is epi.
 The morphism `i` is then automatically an isomorphism. -/
 def Splitting.mk' (h : ShortExact f g) (i : B ⟶ A ⊞ C) (h1 : f ≫ i = biprod.inl)
     (h2 : i ≫ biprod.snd = g) : Splitting f g :=
-  have : IsIso i := isIso_of_shortExact_of_isIso_of_isIso h ⟨exact_inl_snd A C⟩  (𝟙 _) i (𝟙 _)
-    (by aesop_cat) (by aesop_cat)
+  have : IsIso i := isIso_of_shortExact_of_isIso_of_isIso h ⟨exact_inl_snd A C⟩ (𝟙 _) i (𝟙 _)
   { iso := asIso i
     comp_iso_eq_inl := h1
     iso_comp_snd_eq := h2 }
@@ -69,7 +69,6 @@ The morphism `i` is then automatically an isomorphism. -/
 def Splitting.mk'' (h : ShortExact f g) (i : A ⊞ C ⟶ B) (h1 : biprod.inl ≫ i = f)
     (h2 : i ≫ g = biprod.snd) : Splitting f g :=
   have : IsIso i := isIso_of_shortExact_of_isIso_of_isIso ⟨exact_inl_snd A C⟩ h (𝟙 _) i (𝟙 _)
-    (by aesop_cat) (by aesop_cat)
   { iso := (asIso i).symm
     comp_iso_eq_inl := by rw [Iso.symm_hom, asIso_inv, IsIso.comp_inv_eq, h1]
     iso_comp_snd_eq := by rw [Iso.symm_hom, asIso_inv, IsIso.inv_comp_eq, h2] }

Mathlib/Algebra/Homology/Single.lean

@@ -199,6 +199,7 @@ is the same as doing nothing.
 noncomputable def homologyFunctor0Single₀ : single₀ V ⋙ homologyFunctor V _ 0 ≅ 𝟭 V :=
   NatIso.ofComponents (fun X => homology.congr _ _ (by simp) (by simp) ≪≫ homologyZeroZero)
     fun f => by
+      -- Porting note: why can't `aesop_cat` do this?
       dsimp
       ext
       simp
@@ -395,6 +396,7 @@ is the same as doing nothing.
 noncomputable def homologyFunctor0Single₀ : single₀ V ⋙ homologyFunctor V _ 0 ≅ 𝟭 V :=
   NatIso.ofComponents (fun X => homology.congr _ _ (by simp) (by simp) ≪≫ homologyZeroZero)
     fun f => by
+      -- Porting note: why can't `aesop_cat` do this?
       dsimp
       ext
       simp
@@ -462,19 +464,17 @@ variable (V)
 
 /-- `single₀` is the same as `single V _ 0`. -/
 def single₀IsoSingle : single₀ V ≅ single V _ 0 :=
-  NatIso.ofComponents
-    (fun X =>
-      { hom := { f := fun i => by cases i <;> exact 𝟙 _ }
-        inv := { f := fun i => by cases i <;> exact 𝟙 _ }
-        hom_inv_id := from_single₀_ext _ _ (by simp)
-        inv_hom_id := by
-          ext (_|_)
-          . dsimp
-            simp
-          . dsimp
-            rw [Category.id_comp]
-            rfl })
-    fun f => by ext; simp
+  NatIso.ofComponents fun X =>
+    { hom := { f := fun i => by cases i <;> exact 𝟙 _ }
+      inv := { f := fun i => by cases i <;> exact 𝟙 _ }
+      hom_inv_id := from_single₀_ext _ _ (by simp)
+      inv_hom_id := by
+        ext (_|_)
+        . dsimp
+          simp
+        . dsimp
+          rw [Category.id_comp]
+          rfl }
 #align cochain_complex.single₀_iso_single CochainComplex.single₀IsoSingle
 
 instance : Faithful (single₀ V) :=

Mathlib/AlgebraicGeometry/StructureSheaf.lean

@@ -255,7 +255,7 @@ with the `Type` valued structure presheaf.
 -/
 def structurePresheafCompForget :
     structurePresheafInCommRing R ⋙ forget CommRingCat ≅ (structureSheafInType R).1 :=
-  NatIso.ofComponents (fun U => Iso.refl _) (fun i => by aesop)
+  NatIso.ofComponents fun U => Iso.refl _
 set_option linter.uppercaseLean3 false in
 #align algebraic_geometry.structure_presheaf_comp_forget AlgebraicGeometry.structurePresheafCompForget
 

Mathlib/AlgebraicTopology/DoldKan/FunctorN.lean

@@ -55,8 +55,7 @@ def N₁ : SimplicialObject C ⥤ Karoubi (ChainComplex C ℕ) where
       p := PInfty
       idem := PInfty_idem }
   map f :=
-    { f := PInfty ≫ AlternatingFaceMapComplex.map f
-      comm := by aesop_cat }
+    { f := PInfty ≫ AlternatingFaceMapComplex.map f }
 set_option linter.uppercaseLean3 false in
 #align algebraic_topology.dold_kan.N₁ AlgebraicTopology.DoldKan.N₁
 

Mathlib/AlgebraicTopology/DoldKan/GammaCompN.lean

@@ -58,7 +58,7 @@ def Γ₀NondegComplexIso (K : ChainComplex C ℕ) : (Γ₀.splitting K).nondegC
 
 /-- The natural isomorphism `(Γ₀.splitting K).nondegComplex ≅ K` for `K : ChainComplex C ℕ`. -/
 def Γ₀'CompNondegComplexFunctor : Γ₀' ⋙ Split.nondegComplexFunctor ≅ 𝟭 (ChainComplex C ℕ) :=
-  NatIso.ofComponents Γ₀NondegComplexIso (by aesop_cat)
+  NatIso.ofComponents Γ₀NondegComplexIso
 #align algebraic_topology.dold_kan.Γ₀'_comp_nondeg_complex_functor AlgebraicTopology.DoldKan.Γ₀'CompNondegComplexFunctor
 
 /-- The natural isomorphism `Γ₀ ⋙ N₁ ≅ toKaroubi (ChainComplex C ℕ)`. -/

Mathlib/AlgebraicTopology/FundamentalGroupoid/PUnit.lean

@@ -38,11 +38,11 @@ instance {x y : FundamentalGroupoid PUnit} : Subsingleton (x ⟶ y) := by
   apply Quotient.instSubsingletonQuotient
 
 /-- Equivalence of groupoids between fundamental groupoid of punit and punit -/
-def punitEquivDiscretePunit : FundamentalGroupoid PUnit.{u + 1} ≌ Discrete PUnit.{v + 1} :=
+def punitEquivDiscretePUnit : FundamentalGroupoid PUnit.{u + 1} ≌ Discrete PUnit.{v + 1} :=
   CategoryTheory.Equivalence.mk (Functor.star _) ((CategoryTheory.Functor.const _).obj PUnit.unit)
     -- Porting note: was `by decide`
-    (NatIso.ofComponents (fun _ => eqToIso (by simp)) fun _ => by simp)
+    (NatIso.ofComponents fun _ => eqToIso (by simp))
     (Functor.pUnitExt _ _)
-#align fundamental_groupoid.punit_equiv_discrete_punit FundamentalGroupoid.punitEquivDiscretePunit
+#align fundamental_groupoid.punit_equiv_discrete_punit FundamentalGroupoid.punitEquivDiscretePUnit
 
 end FundamentalGroupoid

Mathlib/AlgebraicTopology/SimplicialObject.lean

@@ -809,15 +809,15 @@ object and back is isomorphic to the given object. -/
 @[simps!]
 def SimplicialObject.Augmented.rightOpLeftOpIso (X : SimplicialObject.Augmented C) :
     X.rightOp.leftOp ≅ X :=
-  Comma.isoMk X.left.rightOpLeftOpIso (CategoryTheory.eqToIso <| by aesop_cat) (by aesop_cat)
+  Comma.isoMk X.left.rightOpLeftOpIso (CategoryTheory.eqToIso <| by aesop_cat)
 #align category_theory.simplicial_object.augmented.right_op_left_op_iso CategoryTheory.SimplicialObject.Augmented.rightOpLeftOpIso
 
 /-- Converting an augmented cosimplicial object to an augmented simplicial
 object and back is isomorphic to the given object. -/
 @[simps!]
 def CosimplicialObject.Augmented.leftOpRightOpIso (X : CosimplicialObject.Augmented Cᵒᵖ) :
     X.leftOp.rightOp ≅ X :=
-  Comma.isoMk (CategoryTheory.eqToIso <| by simp) X.right.leftOpRightOpIso (by aesop_cat)
+  Comma.isoMk (CategoryTheory.eqToIso <| by simp) X.right.leftOpRightOpIso
 #align category_theory.cosimplicial_object.augmented.left_op_right_op_iso CategoryTheory.CosimplicialObject.Augmented.leftOpRightOpIso
 
 variable (C)
@@ -867,7 +867,7 @@ def simplicialCosimplicialAugmentedEquiv :
       simp_rw [← op_comp]
       congr 1
       aesop_cat)
-    ((NatIso.ofComponents fun X => X.leftOpRightOpIso) <| by aesop_cat)
+    (NatIso.ofComponents fun X => X.leftOpRightOpIso)
 #align category_theory.simplicial_cosimplicial_augmented_equiv CategoryTheory.simplicialCosimplicialAugmentedEquiv
 
 end CategoryTheory

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -590,8 +590,8 @@ noncomputable def toEquivalence (adj : F ⊣ G) [∀ X, IsIso (adj.unit.app X)]
     where
   functor := F
   inverse := G
-  unitIso := NatIso.ofComponents (fun X => asIso (adj.unit.app X)) (by simp)
-  counitIso := NatIso.ofComponents (fun Y => asIso (adj.counit.app Y)) (by simp)
+  unitIso := NatIso.ofComponents fun X => asIso (adj.unit.app X)
+  counitIso := NatIso.ofComponents fun Y => asIso (adj.counit.app Y)
 #align category_theory.adjunction.to_equivalence CategoryTheory.Adjunction.toEquivalence
 
 /--

Mathlib/CategoryTheory/Adjunction/Comma.lean

@@ -152,7 +152,7 @@ category on `G`. -/
 def mkInitialOfLeftAdjoint (h : F ⊣ G) (A : C) :
     IsInitial (StructuredArrow.mk (h.unit.app A) : StructuredArrow A G)
     where
-  desc B := StructuredArrow.homMk ((h.homEquiv _ _).symm B.pt.hom) (by aesop_cat)
+  desc B := StructuredArrow.homMk ((h.homEquiv _ _).symm B.pt.hom)
   uniq s m _ := by
     apply StructuredArrow.ext
     dsimp
@@ -165,7 +165,7 @@ category on `F`. -/
 def mkTerminalOfRightAdjoint (h : F ⊣ G) (A : D) :
     IsTerminal (CostructuredArrow.mk (h.counit.app A) : CostructuredArrow F A)
     where
-  lift B := CostructuredArrow.homMk (h.homEquiv _ _ B.pt.hom) (by aesop_cat)
+  lift B := CostructuredArrow.homMk (h.homEquiv _ _ B.pt.hom)
   uniq s m _ := by
     apply CostructuredArrow.ext
     dsimp

Mathlib/CategoryTheory/Adjunction/FullyFaithful.lean

@@ -53,14 +53,12 @@ See
 instance unit_isIso_of_L_fully_faithful [Full L] [Faithful L] : IsIso (Adjunction.unit h) :=
   @NatIso.isIso_of_isIso_app _ _ _ _ _ _ (Adjunction.unit h) fun X =>
     @Yoneda.isIso _ _ _ _ ((Adjunction.unit h).app X)
-      ⟨⟨{ app := fun Y f => L.preimage ((h.homEquiv (unop Y) (L.obj X)).symm f),
-          naturality := fun X Y f => by
-            funext x -- porting note: `aesop_cat` is not able to do `funext` automatically
-            aesop_cat },
+      ⟨⟨{ app := fun Y f => L.preimage ((h.homEquiv (unop Y) (L.obj X)).symm f) },
           ⟨by
             ext x
             apply L.map_injective
-            aesop_cat, by
+            aesop_cat,
+           by
             ext x
             dsimp
             simp only [Adjunction.homEquiv_counit, preimage_comp, preimage_map, Category.assoc]
@@ -77,14 +75,12 @@ instance counit_isIso_of_R_fully_faithful [Full R] [Faithful R] : IsIso (Adjunct
   @NatIso.isIso_of_isIso_app _ _ _ _ _ _ (Adjunction.counit h) fun X =>
     @isIso_of_op _ _ _ _ _ <|
       @Coyoneda.isIso _ _ _ _ ((Adjunction.counit h).app X).op
-        ⟨⟨{ app := fun Y f => R.preimage ((h.homEquiv (R.obj X) Y) f),
-            naturality := fun X Y f => by
-              funext x
-              aesop_cat },
+        ⟨⟨{ app := fun Y f => R.preimage ((h.homEquiv (R.obj X) Y) f) },
             ⟨by
               ext x
               apply R.map_injective
-              simp, by
+              simp,
+             by
               ext x
               dsimp
               simp only [Adjunction.homEquiv_unit, preimage_comp, preimage_map]