Merge master into nightly-testing

Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean

@@ -318,7 +318,7 @@ noncomputable def sheafify : SheafOfModules.{v} R where
 def toSheafify : M₀ ⟶ (restrictScalars α).obj (sheafify α φ).val :=
   homMk φ (fun X r₀ m₀ ↦ by
     simpa using (Sheafify.map_smul_eq α φ (α.app _ r₀) (φ.app _ m₀) (𝟙 _)
-      r₀ (by aesop) m₀ (by simp)).symm)
+      r₀ (by simp) m₀ (by simp)).symm)
 
 lemma toSheafify_app_apply (X : Cᵒᵖ) (x : M₀.obj X) :
     ((toSheafify α φ).app X).hom x = φ.app X x := rfl

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

@@ -85,8 +85,7 @@ theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟶ N} (x : LinearMap
   suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f ≪≫ kernelIsoKer f).inv) x = x by
     convert this
   rw [Iso.trans_inv, ← LinearMap.coe_comp, ← hom_comp, Category.assoc]
-  simp only [Category.assoc, kernelSubobject_arrow', kernelIsoKer_inv_kernel_ι]
-  aesop_cat
+  simp
 
 /-- An extensionality lemma showing that two elements of a cokernel by an image
 are equal if they differ by an element of the image.

Mathlib/Algebra/Category/Semigrp/Basic.lean

@@ -44,7 +44,7 @@ namespace MagmaCat
 @[to_additive]
 instance bundledHom : BundledHom @MulHom :=
   ⟨@MulHom.toFun, @MulHom.id, @MulHom.comp,
-    by intros; apply @DFunLike.coe_injective, by aesop_cat, by aesop_cat⟩
+    by intros; apply @DFunLike.coe_injective, by aesop_cat, by simp⟩
 
 -- Porting note: deriving failed for `ConcreteCategory`,
 -- "default handlers have not been implemented yet"

Mathlib/Algebra/Homology/Additive.lean

@@ -176,7 +176,7 @@ theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : W
     (α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) :
     (F.mapHomologicalComplex c).map f ≫ (NatTrans.mapHomologicalComplex α c).app D =
       (NatTrans.mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f := by
-  aesop_cat
+  simp
 
 /-- A natural isomorphism between functors induces a natural isomorphism
 between those functors applied to homological complexes.

Mathlib/Algebra/Homology/Augment.lean

@@ -37,7 +37,7 @@ The components of this chain map are `C.d 1 0` in degree 0, and zero otherwise.
 -/
 def truncateTo [HasZeroObject V] [HasZeroMorphisms V] (C : ChainComplex V ℕ) :
     truncate.obj C ⟶ (single₀ V).obj (C.X 0) :=
-  (toSingle₀Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 1 0, by aesop⟩
+  (toSingle₀Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 1 0, by simp⟩
 
 -- PROJECT when `V` is abelian (but not generally?)
 -- `[∀ n, Exact (C.d (n+2) (n+1)) (C.d (n+1) n)] [Epi (C.d 1 0)]` iff `QuasiIso (C.truncate_to)`
@@ -204,7 +204,7 @@ The components of this chain map are `C.d 0 1` in degree 0, and zero otherwise.
 -/
 def toTruncate [HasZeroObject V] [HasZeroMorphisms V] (C : CochainComplex V ℕ) :
     (single₀ V).obj (C.X 0) ⟶ truncate.obj C :=
-  (fromSingle₀Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 0 1, by aesop⟩
+  (fromSingle₀Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 0 1, by simp⟩
 
 variable [HasZeroMorphisms V]
 

Mathlib/Algebra/Homology/HomologicalBicomplex.lean

@@ -177,15 +177,15 @@ def flipEquivalenceUnitIso :
     𝟭 (HomologicalComplex₂ C c₁ c₂) ≅ flipFunctor C c₁ c₂ ⋙ flipFunctor C c₂ c₁ :=
   NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun i₁ =>
     HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
-    (by aesop_cat)) (by aesop_cat)) (by aesop_cat)
+    (by simp)) (by aesop_cat)) (by aesop_cat)
 
 /-- Auxiliary definition for `HomologicalComplex₂.flipEquivalence`. -/
 @[simps!]
 def flipEquivalenceCounitIso :
     flipFunctor C c₂ c₁ ⋙ flipFunctor C c₁ c₂ ≅ 𝟭 (HomologicalComplex₂ C c₂ c₁) :=
   NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun i₂ =>
     HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
-    (by aesop_cat)) (by aesop_cat)) (by aesop_cat)
+    (by simp)) (by aesop_cat)) (by aesop_cat)
 
 /-- Flipping a complex of complexes over the diagonal, as an equivalence of categories. -/
 @[simps]

Mathlib/Algebra/Homology/HomologySequence.lean

@@ -165,7 +165,7 @@ noncomputable def composableArrows₃Functor [CategoryWithHomology C] :
     HomologicalComplex C c ⥤ ComposableArrows C 3 where
   obj K := composableArrows₃ K i j
   map {K L} φ := ComposableArrows.homMk₃ (homologyMap φ i) (opcyclesMap φ i) (cyclesMap φ j)
-    (homologyMap φ j) (by aesop_cat) (by aesop_cat) (by aesop_cat)
+    (homologyMap φ j) (by simp) (by simp) (by simp)
 
 end HomologySequence
 
@@ -311,7 +311,7 @@ lemma homology_exact₂ : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i
     have e : S.map (HomologicalComplex.homologyFunctor C c i) ≅
         S.map (HomologicalComplex.opcyclesFunctor C c i) :=
       ShortComplex.isoMk (asIso (S.X₁.homologyι i))
-        (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by aesop_cat) (by aesop_cat)
+        (asIso (S.X₂.homologyι i)) (asIso (S.X₃.homologyι i)) (by simp) (by simp)
     exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)
 
 /-- Exactness of `S.X₂.homology i ⟶ S.X₃.homology i ⟶ S.X₁.homology j`. -/

Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean

@@ -201,7 +201,7 @@ noncomputable def triangleRotateIsoTriangleOfDegreewiseSplit :
     (triangle φ).rotate ≅
       triangleOfDegreewiseSplit _ (triangleRotateShortComplexSplitting φ) :=
   Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _)
-    (by aesop_cat) (by aesop_cat) (by ext; dsimp; simp)
+    (by simp) (by simp) (by ext; dsimp; simp)
 
 /-- The triangle `(triangleh φ).rotate` is isomorphic to a triangle attached to a
 degreewise split short exact sequence of cochain complexes. -/

Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean

@@ -50,9 +50,9 @@ def inverse : (J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C) where
 @[simps!]
 def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C :=
   NatIso.ofComponents (fun _ => isoMk
-    (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
-    (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
-    (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
+    (NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
+    (NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
+    (NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
     (by aesop_cat) (by aesop_cat)) (by aesop_cat)
 
 /-- The counit isomorphism of the equivalence
@@ -61,7 +61,7 @@ def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C :=
 def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _ :=
   NatIso.ofComponents (fun _ => NatIso.ofComponents
     (fun _ => isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
-      (by aesop_cat) (by aesop_cat)) (by aesop_cat)) (by aesop_cat)
+      (by simp) (by simp)) (by aesop_cat)) (by aesop_cat)
 
 end FunctorEquivalence
 

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

@@ -50,7 +50,7 @@ when `c.prev j = i` and `c.next j = k`. -/
 noncomputable def natIsoSc' (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k) :
     shortComplexFunctor C c j ≅ shortComplexFunctor' C c i j k :=
   NatIso.ofComponents (fun K => ShortComplex.isoMk (K.XIsoOfEq hi) (Iso.refl _) (K.XIsoOfEq hk)
-    (by aesop_cat) (by aesop_cat)) (by aesop_cat)
+    (by simp) (by simp)) (by aesop_cat)
 
 variable {C c}
 

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -1008,7 +1008,7 @@ lemma hasCokernel [S.HasLeftHomology] [HasKernel S.g] :
   haveI : HasColimit (parallelPair h.f' 0) := ⟨⟨⟨_, h.hπ'⟩⟩⟩
   let e : parallelPair (kernel.lift S.g S.f S.zero) 0 ≅ parallelPair h.f' 0 :=
     parallelPair.ext (Iso.refl _) (IsLimit.conePointUniqueUpToIso (kernelIsKernel S.g) h.hi)
-      (by aesop_cat) (by aesop_cat)
+      (by aesop_cat) (by simp)
   exact hasColimitOfIso e
 
 end HasLeftHomology

Mathlib/Algebra/Homology/ShortComplex/Limits.lean

@@ -66,7 +66,7 @@ noncomputable def limitCone : Cone F :=
   Cone.mk (ShortComplex.mk (limMap (whiskerLeft F π₁Toπ₂)) (limMap (whiskerLeft F π₂Toπ₃))
       (by aesop_cat))
     { app := fun j => Hom.mk (limit.π _ _) (limit.π _ _) (limit.π _ _)
-        (by aesop_cat) (by aesop_cat)
+        (by simp) (by simp)
       naturality := fun _ _ f => by
         ext
         all_goals
@@ -199,7 +199,7 @@ noncomputable def colimitCocone : Cocone F :=
   Cocone.mk (ShortComplex.mk (colimMap (whiskerLeft F π₁Toπ₂)) (colimMap (whiskerLeft F π₂Toπ₃))
       (by aesop_cat))
     { app := fun j => Hom.mk (colimit.ι (F ⋙ π₁) _) (colimit.ι (F ⋙ π₂) _)
-        (colimit.ι (F ⋙ π₃) _) (by aesop_cat) (by aesop_cat)
+        (colimit.ι (F ⋙ π₃) _) (by simp) (by simp)
       naturality := fun _ _ f => by
         ext
         · dsimp; erw [comp_id, colimit.w (F ⋙ π₁)]

Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

@@ -834,7 +834,7 @@ lemma preservesLeftHomology_of_zero_g (hg : S.g = 0)
     f' := by
       have := h.isIso_i hg
       let e : parallelPair h.f' 0 ≅ parallelPair S.f 0 :=
-        parallelPair.ext (Iso.refl _) (asIso h.i) (by aesop_cat) (by aesop_cat)
+        parallelPair.ext (Iso.refl _) (asIso h.i) (by simp) (by simp)
       exact Limits.preservesColimit_of_iso_diagram F e.symm}⟩
 
 /-- If a short complex `S` is such that `S.f = 0` and that the kernel of `S.g` is preserved
@@ -848,7 +848,7 @@ lemma preservesRightHomology_of_zero_f (hf : S.f = 0)
     g' := by
       have := h.isIso_p hf
       let e : parallelPair S.g 0 ≅ parallelPair h.g' 0 :=
-        parallelPair.ext (asIso h.p) (Iso.refl _) (by aesop_cat) (by aesop_cat)
+        parallelPair.ext (asIso h.p) (Iso.refl _) (by simp) (by simp)
       exact Limits.preservesLimit_of_iso_diagram F e }⟩
 
 end Functor

Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

@@ -150,7 +150,7 @@ def ofIsLimitKernelFork (hf : S.f = 0) (c : KernelFork S.g) (hc : IsLimit c) :
   wp := by rw [comp_id, hf]
   hp := CokernelCofork.IsColimit.ofId _ hf
   wι := KernelFork.condition _
-  hι := IsLimit.ofIsoLimit hc (Fork.ext (Iso.refl _) (by aesop_cat))
+  hι := IsLimit.ofIsoLimit hc (Fork.ext (Iso.refl _) (by simp))
 
 @[simp] lemma ofIsLimitKernelFork_g' (hf : S.f = 0) (c : KernelFork S.g)
     (hc : IsLimit c) : (ofIsLimitKernelFork S hf c hc).g' = S.g := by
@@ -173,7 +173,7 @@ def ofIsColimitCokernelCofork (hg : S.g = 0) (c : CokernelCofork S.f) (hc : IsCo
   p := c.π
   ι := 𝟙 _
   wp := CokernelCofork.condition _
-  hp := IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by aesop_cat))
+  hp := IsColimit.ofIsoColimit hc (Cofork.ext (Iso.refl _) (by simp))
   wι := Cofork.IsColimit.hom_ext hc (by simp [hg])
   hι := KernelFork.IsLimit.ofId _ (Cofork.IsColimit.hom_ext hc (by simp [hg]))
 
@@ -1287,7 +1287,7 @@ lemma hasKernel [S.HasRightHomology] [HasCokernel S.f] :
   haveI : HasLimit (parallelPair h.g' 0) := ⟨⟨⟨_, h.hι'⟩⟩⟩
   let e : parallelPair (cokernel.desc S.f S.g S.zero) 0 ≅ parallelPair h.g' 0 :=
     parallelPair.ext (IsColimit.coconePointUniqueUpToIso (colimit.isColimit _) h.hp)
-      (Iso.refl _) (coequalizer.hom_ext (by simp)) (by aesop_cat)
+      (Iso.refl _) (coequalizer.hom_ext (by simp)) (by simp)
   exact hasLimitOfIso e.symm
 
 end HasRightHomology

Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

@@ -345,7 +345,7 @@ lemma op_δ : S.op.δ = S.δ.op := Quiver.Hom.unop_inj (by
 
 /-- The duality isomorphism `S.L₂'.op ≅ S.op.L₁'`. -/
 noncomputable def L₂'OpIso : S.L₂'.op ≅ S.op.L₁' :=
-  ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat)
+  ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp)
     (by dsimp; simp only [id_comp, comp_id, S.op_δ])
 
 /-- Exactness of `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`. -/
@@ -475,7 +475,7 @@ noncomputable def functorP : SnakeInput C ⥤ C where
   obj S := S.P
   map f := pullback.map _ _ _ _ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ f.f₁.comm₂₃.symm
       (congr_arg ShortComplex.Hom.τ₃ f.comm₀₁.symm)
-  map_id _ := by dsimp [P]; aesop_cat
+  map_id _ := by dsimp [P]; simp
   map_comp _ _ := by dsimp [P]; aesop_cat
 
 @[reassoc]

Mathlib/Algebra/Homology/Single.lean

@@ -220,7 +220,7 @@ noncomputable def toSingle₀Equiv (C : ChainComplex V ℕ) (X : V) :
     obtain rfl : i = 1 := by simpa using hi.symm
     exact f.2)
   left_inv φ := by aesop_cat
-  right_inv f := by aesop_cat
+  right_inv f := by simp
 
 @[simp]
 lemma toSingle₀Equiv_symm_apply_f_zero {C : ChainComplex V ℕ} {X : V}

Mathlib/Algebra/Lie/Weights/Basic.lean

@@ -228,7 +228,7 @@ variable {M}
 @[ext] lemma ext {χ₁ χ₂ : Weight R L M} (h : ∀ x, χ₁ x = χ₂ x) : χ₁ = χ₂ := by
   cases' χ₁ with f₁ _; cases' χ₂ with f₂ _; aesop
 
-lemma ext_iff' {χ₁ χ₂ : Weight R L M} : (χ₁ : L → R) = χ₂ ↔ χ₁ = χ₂ := by aesop
+lemma ext_iff' {χ₁ χ₂ : Weight R L M} : (χ₁ : L → R) = χ₂ ↔ χ₁ = χ₂ := by simp
 
 lemma exists_ne_zero (χ : Weight R L M) :
     ∃ x ∈ genWeightSpace M χ, x ≠ 0 := by

Mathlib/Algebra/Module/Presentation/Basic.lean

@@ -354,8 +354,8 @@ certain linear equations. -/
 noncomputable def linearMapEquiv : (M →ₗ[A] N) ≃ relations.Solution N where
   toFun f := solution.postcomp f
   invFun s := h.desc s
-  left_inv f := h.postcomp_injective (by aesop)
-  right_inv s := by aesop
+  left_inv f := h.postcomp_injective (by simp)
+  right_inv s := by simp
 
 section
 

Mathlib/Algebra/Module/Submodule/Pointwise.lean

@@ -475,8 +475,8 @@ lemma mem_singleton_set_smul [SMulCommClass R S M] (r : S) (x : M) :
       exact ⟨t • n, by aesop,  smul_comm _ _ _⟩
     · rcases h₁ with ⟨m₁, h₁, rfl⟩
       rcases h₂ with ⟨m₂, h₂, rfl⟩
-      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by aesop⟩
-    · exact ⟨0, Submodule.zero_mem _, by aesop⟩
+      exact ⟨m₁ + m₂, Submodule.add_mem _ h₁ h₂, by simp⟩
+    · exact ⟨0, Submodule.zero_mem _, by simp⟩
   · aesop
 
 lemma smul_inductionOn_pointwise [SMulCommClass S R M] {a : S} {p : (x : M) → x ∈ a • N → Prop}

Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean

@@ -142,7 +142,7 @@ theorem t1Space_iff_isField [IsDomain R] : T1Space (PrimeSpectrum R) ↔ IsField
         (mt
           (Ring.ne_bot_of_isMaximal_of_not_isField <|
             (isClosed_singleton_iff_isMaximal _).1 (T1Space.t1 ⟨⊥, hbot⟩))
-          (by aesop))
+          (by simp))
   · refine ⟨fun x => (isClosed_singleton_iff_isMaximal x).2 ?_⟩
     by_cases hx : x.asIdeal = ⊥
     · letI := h.toSemifield

Mathlib/AlgebraicTopology/CechNerve.lean

@@ -50,7 +50,7 @@ variable [∀ n : ℕ, HasWidePullback.{0} f.right (fun _ : Fin (n + 1) => f.lef
 def cechNerve : SimplicialObject C where
   obj n := widePullback.{0} f.right (fun _ : Fin (n.unop.len + 1) => f.left) fun _ => f.hom
   map g := WidePullback.lift (WidePullback.base _)
-    (fun i => WidePullback.π _ (g.unop.toOrderHom i)) (by aesop_cat)
+    (fun i => WidePullback.π _ (g.unop.toOrderHom i)) (by simp)
 
 /-- The morphism between Čech nerves associated to a morphism of arrows. -/
 @[simps]

Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean

@@ -834,7 +834,7 @@ 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)
+  Comma.isoMk X.left.rightOpLeftOpIso (CategoryTheory.eqToIso <| by simp)
 
 /-- Converting an augmented cosimplicial object to an augmented simplicial
 object and back is isomorphic to the given object. -/

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean

@@ -724,7 +724,7 @@ variable [Ring A] [StarRing A] [Algebra R A] [ContinuousFunctionalCalculus R p]
 lemma isUnit_cfc_iff (f : R → R) (a : A) (hf : ContinuousOn f (spectrum R a) := by cfc_cont_tac)
     (ha : p a := by cfc_tac) : IsUnit (cfc f a) ↔ ∀ x ∈ spectrum R a, f x ≠ 0 := by
   rw [← spectrum.zero_not_mem_iff R, cfc_map_spectrum ..]
-  aesop
+  simp
 
 alias ⟨_, isUnit_cfc⟩ := isUnit_cfc_iff
 

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean

@@ -152,7 +152,7 @@ lemma log_pow (n : ℕ) (a : A) (ha₂ : ∀ x ∈ spectrum ℝ a, 0 < x)
 variable [CompleteSpace A]
 
 lemma log_exp (a : A) (ha : IsSelfAdjoint a := by cfc_tac) : log (NormedSpace.exp ℝ a) = a := by
-  have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := aesop)
+  have hcont : ContinuousOn Real.log (Real.exp '' spectrum ℝ a) := by fun_prop (disch := simp)
   rw [log, ← real_exp_eq_normedSpace_exp, ← cfc_comp' Real.log Real.exp a hcont]
   simp [cfc_id' (R := ℝ) a]
 

Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean

@@ -365,7 +365,7 @@ lemma sqrt_rpow_nnreal {a : A} {x : ℝ≥0} : sqrt (a ^ (x : ℝ)) = a ^ (x / 2
     by_cases hx : x = 0
     case pos => simp [hx, rpow_zero _ htriv]
     case neg =>
-      have h₁ : 0 < x := lt_of_le_of_ne (by aesop) (Ne.symm hx)
+      have h₁ : 0 < x := lt_of_le_of_ne (by simp) (Ne.symm hx)
       have h₂ : (x : ℝ) / 2 = NNReal.toReal (x / 2) := rfl
       have h₃ : 0 < x / 2 := by positivity
       rw [← nnrpow_eq_rpow h₁, h₂, ← nnrpow_eq_rpow h₃, sqrt_nnrpow (A := A)]

Mathlib/Analysis/SpecificLimits/Basic.lean

@@ -109,7 +109,7 @@ theorem Filter.EventuallyEq.div_mul_cancel_atTop {α K : Type*} [LinearOrderedSe
     {f g : α → K} {l : Filter α} (hg : Tendsto g l atTop) :
     (fun x ↦ f x / g x * g x) =ᶠ[l] fun x ↦ f x :=
   div_mul_cancel <| hg.mono_right <| le_principal_iff.mpr <|
-    mem_of_superset (Ioi_mem_atTop 0) <| by aesop
+    mem_of_superset (Ioi_mem_atTop 0) <| by simp
 
 /-- If when `x` tends to `∞`, `g` tends to `∞` and `f x / g x` tends to a positive
   constant, then `f` tends to `∞`. -/

Mathlib/CategoryTheory/Abelian/Exact.lean

@@ -105,7 +105,7 @@ def Exact.isLimitImage (h : S.Exact) :
   rw [exact_iff_kernel_ι_comp_cokernel_π_zero] at h
   exact KernelFork.IsLimit.ofι _ _
     (fun u hu ↦ kernel.lift (cokernel.π S.f) u
-      (by rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero])) (by aesop_cat)
+      (by rw [← kernel.lift_ι S.g u hu, Category.assoc, h, comp_zero])) (by simp)
     (fun _ _ _ hm => by rw [← cancel_mono (Abelian.image.ι S.f), hm, kernel.lift_ι])
 
 /-- If `(f, g)` is exact, then `image.ι f` is a kernel of `g`. -/
@@ -123,7 +123,7 @@ def Exact.isColimitCoimage (h : S.Exact) :
   refine CokernelCofork.IsColimit.ofπ _ _
     (fun u hu => cokernel.desc (kernel.ι S.g) u
       (by rw [← cokernel.π_desc S.f u hu, ← Category.assoc, h, zero_comp]))
-    (by aesop_cat) ?_
+    (by simp) ?_
   intros _ _ _ _ hm
   ext
   rw [hm, cokernel.π_desc]

Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean

@@ -240,7 +240,7 @@ lemma InjectiveResolution.iso_hom_naturality {X Y : C} (f : X ⟶ Y)
       I.iso.hom ≫ (HomotopyCategory.quotient _ _).map φ := by
   apply HomotopyCategory.eq_of_homotopy
   apply descHomotopy f
-  all_goals aesop_cat
+  all_goals aesop
 
 @[reassoc]
 lemma InjectiveResolution.iso_inv_naturality {X Y : C} (f : X ⟶ Y)

Mathlib/CategoryTheory/Action/Limits.lean

@@ -209,7 +209,7 @@ variable [HasZeroMorphisms V]
 
 -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10688): in order to ease automation, the `Zero` instance is introduced separately,
 -- and the lemma `Action.zero_hom` was moved just below
-instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by aesop_cat⟩
+instance {X Y : Action V G} : Zero (X ⟶ Y) := ⟨0, by simp⟩
 
 @[simp]
 theorem zero_hom {X Y : Action V G} : (0 : X ⟶ Y).hom = 0 :=

Mathlib/CategoryTheory/Action/Monoidal.lean

@@ -89,7 +89,7 @@ variable [BraidedCategory V]
 
 instance : BraidedCategory (Action V G) :=
   braidedCategoryOfFaithful (Action.forget V G) (fun X Y => mkIso (β_ _ _)
-    (fun g => by simp [FunctorCategoryEquivalence.inverse])) (by aesop_cat)
+    (fun g => by simp [FunctorCategoryEquivalence.inverse])) (by simp)
 
 /-- When `V` is braided the forgetful functor `Action V G` to `V` is braided. -/
 instance : (Action.forget V G).Braided where

Mathlib/CategoryTheory/Adjunction/Basic.lean

@@ -293,14 +293,14 @@ theorem eq_homEquiv_apply {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B
 def corepresentableBy (X : C) :
     (G ⋙ coyoneda.obj (Opposite.op X)).CorepresentableBy (F.obj X) where
   homEquiv := adj.homEquiv _ _
-  homEquiv_comp := by aesop_cat
+  homEquiv_comp := by simp
 
 /--  If `adj : F ⊣ G`, and `Y : D`, then `G.obj Y` represents `X ↦ (F.obj X ⟶ Y)`-/
 @[simps]
 def representableBy (Y : D) :
     (F.op ⋙ yoneda.obj Y).RepresentableBy (G.obj Y) where
   homEquiv := (adj.homEquiv _ _).symm
-  homEquiv_comp := by aesop_cat
+  homEquiv_comp := by simp
 
 end