diff --git a/.github/build.in.yml b/.github/build.in.yml
index c56faf4061fea..b7acc84572050 100644
--- a/.github/build.in.yml
+++ b/.github/build.in.yml
@@ -12,19 +12,14 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.12.1
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository MAIN_OR_FORK 'leanprover-community/mathlib4'
     name: Lint styleJOB_NAME
diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml
index 869b4d379c959..37c0ac50d19a0 100644
--- a/.github/workflows/bors.yml
+++ b/.github/workflows/bors.yml
@@ -22,19 +22,14 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.12.1
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style
diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index 25c242698e644..62525af3c3089 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -29,19 +29,14 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.12.1
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository == 'leanprover-community/mathlib4'
     name: Lint style
diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml
index 9848f1817b72d..14ae2662c9d09 100644
--- a/.github/workflows/build_fork.yml
+++ b/.github/workflows/build_fork.yml
@@ -26,19 +26,14 @@ env:
   # not necessarily satisfy this property.
   LAKE_NO_CACHE: true
 
-jobs:
-  # Cancels previous runs of jobs in this file
-  cancel:
-    if: github.repository == 'leanprover-community/mathlib4'
-    name: 'Cancel Previous Runs (CI)'
-    runs-on: ubuntu-latest
-    # timeout-minutes: 3
-    steps:
-      - uses: styfle/cancel-workflow-action@0.12.1
-        with:
-          all_but_latest: true
-          access_token: ${{ github.token }}
+concurrency:
+  # label each workflow run; only the latest with each label will run
+  # workflows on master get more expressive labels
+  group: ${{ github.workflow }}-${{ github.ref }}.${{(github.ref == 'refs/heads/master' && github.run_id) || ''}}
+  # cancel any running workflow with the same label
+  cancel-in-progress: true
 
+jobs:
   style_lint:
     if: github.repository != 'leanprover-community/mathlib4'
     name: Lint style (fork)
diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
index d1dec86a2c040..440f20249af9e 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.lean
+++ b/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
diff --git a/Mathlib/Algebra/Category/ModuleCat/Subobject.lean b/Mathlib/Algebra/Category/ModuleCat/Subobject.lean
index 8b5e532a67127..5fb8394a9c465 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Subobject.lean
+++ b/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.
diff --git a/Mathlib/Algebra/Category/Semigrp/Basic.lean b/Mathlib/Algebra/Category/Semigrp/Basic.lean
index d30f2b19f232e..e6e54e5ccab88 100644
--- a/Mathlib/Algebra/Category/Semigrp/Basic.lean
+++ b/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"
diff --git a/Mathlib/Algebra/Homology/Additive.lean b/Mathlib/Algebra/Homology/Additive.lean
index 1b14c45bf5b00..86d5e417b4051 100644
--- a/Mathlib/Algebra/Homology/Additive.lean
+++ b/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.
diff --git a/Mathlib/Algebra/Homology/Augment.lean b/Mathlib/Algebra/Homology/Augment.lean
index b7701f75f0d90..2f19bc16f99bb 100644
--- a/Mathlib/Algebra/Homology/Augment.lean
+++ b/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]
 
diff --git a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
index 634f2df3056f2..e9f7ce59fdfb9 100644
--- a/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
+++ b/Mathlib/Algebra/Homology/HomologicalBicomplex.lean
@@ -177,7 +177,7 @@ 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!]
@@ -185,7 +185,7 @@ 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]
diff --git a/Mathlib/Algebra/Homology/HomologicalComplex.lean b/Mathlib/Algebra/Homology/HomologicalComplex.lean
index 03b17997ea652..9fc057de9025d 100644
--- a/Mathlib/Algebra/Homology/HomologicalComplex.lean
+++ b/Mathlib/Algebra/Homology/HomologicalComplex.lean
@@ -566,7 +566,7 @@ attribute [simp] comm_to_apply
 induces a morphism of arrows of the differentials out of each object.
 -/
 def sqFrom (f : Hom C₁ C₂) (i : ι) : Arrow.mk (C₁.dFrom i) ⟶ Arrow.mk (C₂.dFrom i) :=
-  Arrow.homMk (f.comm_from i)
+  Arrow.homMk _ _ (f.comm_from i)
 
 @[simp]
 theorem sqFrom_left (f : Hom C₁ C₂) (i : ι) : (f.sqFrom i).left = f.f i :=
@@ -589,7 +589,7 @@ theorem sqFrom_comp (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι) :
 induces a morphism of arrows of the differentials into each object.
 -/
 def sqTo (f : Hom C₁ C₂) (j : ι) : Arrow.mk (C₁.dTo j) ⟶ Arrow.mk (C₂.dTo j) :=
-  Arrow.homMk (f.comm_to j)
+  Arrow.homMk _ _ (f.comm_to j)
 
 @[simp]
 theorem sqTo_left (f : Hom C₁ C₂) (j : ι) : (f.sqTo j).left = f.prev j :=
diff --git a/Mathlib/Algebra/Homology/HomologySequence.lean b/Mathlib/Algebra/Homology/HomologySequence.lean
index 6a325db2f53a9..c3743d891f42f 100644
--- a/Mathlib/Algebra/Homology/HomologySequence.lean
+++ b/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`. -/
diff --git a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean b/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
index cabff6665b54e..c454aa0ad7d69 100644
--- a/Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
+++ b/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. -/
diff --git a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean
index 3e5b25181998c..b16976a6c8d8f 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean
+++ b/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
 
diff --git a/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean b/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
index 415cac78ef15f..97bd4dc2b02fa 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
+++ b/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}
 
diff --git a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
index a8abcedd4972c..8778624055502 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
+++ b/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
diff --git a/Mathlib/Algebra/Homology/ShortComplex/Limits.lean b/Mathlib/Algebra/Homology/ShortComplex/Limits.lean
index 1f94e0fc71c5e..a7a46d412c3f3 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/Limits.lean
+++ b/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 ⋙ π₁)]
diff --git a/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
index eacf12a85c953..df003423f5f9d 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean
+++ b/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
diff --git a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean b/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
index 9832970621a74..b6c4767c9e7b7 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
+++ b/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
diff --git a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean b/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
index 8fe3dbac06932..c3abf86cbb643 100644
--- a/Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
+++ b/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]
diff --git a/Mathlib/Algebra/Homology/Single.lean b/Mathlib/Algebra/Homology/Single.lean
index a9cbef23cd3c9..b6dc763c87a95 100644
--- a/Mathlib/Algebra/Homology/Single.lean
+++ b/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}
diff --git a/Mathlib/Algebra/Lie/Weights/Basic.lean b/Mathlib/Algebra/Lie/Weights/Basic.lean
index 7ecb88285cfc7..9cb657c719f2d 100644
--- a/Mathlib/Algebra/Lie/Weights/Basic.lean
+++ b/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
diff --git a/Mathlib/Algebra/Module/Presentation/Basic.lean b/Mathlib/Algebra/Module/Presentation/Basic.lean
index b12188e759ad7..e9c9735f6af10 100644
--- a/Mathlib/Algebra/Module/Presentation/Basic.lean
+++ b/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
 
diff --git a/Mathlib/Algebra/Module/Submodule/Pointwise.lean b/Mathlib/Algebra/Module/Submodule/Pointwise.lean
index bad57cad693c0..b3c2fa905b8d3 100644
--- a/Mathlib/Algebra/Module/Submodule/Pointwise.lean
+++ b/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}
diff --git a/Mathlib/Algebra/Star/SelfAdjoint.lean b/Mathlib/Algebra/Star/SelfAdjoint.lean
index 2acc10366d170..b43afd4b955f9 100644
--- a/Mathlib/Algebra/Star/SelfAdjoint.lean
+++ b/Mathlib/Algebra/Star/SelfAdjoint.lean
@@ -563,10 +563,10 @@ theorem isSelfAdjoint_smul_of_mem_skewAdjoint [Ring R] [AddCommGroup A] [Module
     (ha : a ∈ skewAdjoint A) : IsSelfAdjoint (r • a) :=
   (star_smul _ _).trans <| (congr_arg₂ _ hr ha).trans <| neg_smul_neg _ _
 
-instance isStarNormal_zero [Semiring R] [StarRing R] : IsStarNormal (0 : R) :=
+protected instance IsStarNormal.zero [Semiring R] [StarRing R] : IsStarNormal (0 : R) :=
   ⟨by simp only [Commute.refl, star_comm_self, star_zero]⟩
 
-instance isStarNormal_one [MulOneClass R] [StarMul R] : IsStarNormal (1 : R) :=
+protected instance IsStarNormal.one [MulOneClass R] [StarMul R] : IsStarNormal (1 : R) :=
   ⟨by simp only [Commute.refl, star_comm_self, star_one]⟩
 
 protected instance IsStarNormal.star [Mul R] [StarMul R] {x : R} [IsStarNormal x] :
@@ -577,6 +577,10 @@ protected instance IsStarNormal.neg [Ring R] [StarAddMonoid R] {x : R} [IsStarNo
     IsStarNormal (-x) :=
   ⟨show star (-x) * -x = -x * star (-x) by simp_rw [star_neg, neg_mul_neg, star_comm_self']⟩
 
+protected instance IsStarNormal.val_inv [Monoid R] [StarMul R] {x : Rˣ} [IsStarNormal (x : R)] :
+    IsStarNormal (↑x⁻¹ : R) where
+  star_comm_self := by simpa [← Units.coe_star_inv, -Commute.units_val_iff] using star_comm_self
+
 protected instance IsStarNormal.map {F R S : Type*} [Mul R] [Star R] [Mul S] [Star S]
     [FunLike F R S] [MulHomClass F R S] [StarHomClass F R S] (f : F) (r : R) [hr : IsStarNormal r] :
     IsStarNormal (f r) where
diff --git a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean b/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
index 680ed47f8dce6..2eabfbfe9f773 100644
--- a/Mathlib/AlgebraicGeometry/PrimeSpectrum/Basic.lean
+++ b/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
diff --git a/Mathlib/AlgebraicTopology/CechNerve.lean b/Mathlib/AlgebraicTopology/CechNerve.lean
index 667421531fc21..1a6755cccda6b 100644
--- a/Mathlib/AlgebraicTopology/CechNerve.lean
+++ b/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]
diff --git a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
index c8235ee654872..cf5fcca453bd2 100644
--- a/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
+++ b/Mathlib/AlgebraicTopology/DoldKan/Compatibility.lean
@@ -122,8 +122,8 @@ theorem equivalence₂CounitIso_eq :
     (equivalence₂ eB hF).counitIso = equivalence₂CounitIso eB hF := by
   ext Y'
   dsimp [equivalence₂, Iso.refl]
-  simp only [equivalence₁CounitIso_eq, equivalence₂CounitIso_hom_app,
-    equivalence₁CounitIso_hom_app, Functor.map_comp, assoc]
+  simp only [equivalence₁CounitIso_eq, equivalence₁CounitIso_hom_app, comp_id, id_comp,
+    Functor.map_comp, assoc, equivalence₂CounitIso_hom_app]
 
 /-- The unit isomorphism of the equivalence `equivalence₂` between `A` and `B`. -/
 @[simps!]
@@ -138,8 +138,8 @@ def equivalence₂UnitIso : 𝟭 A ≅ (F ⋙ eB.inverse) ⋙ eB.functor ⋙ e'.
 theorem equivalence₂UnitIso_eq : (equivalence₂ eB hF).unitIso = equivalence₂UnitIso eB hF := by
   ext X
   dsimp [equivalence₂]
-  simp only [equivalence₂UnitIso_hom_app, equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app,
-      assoc, NatIso.cancel_natIso_hom_left]
+  simp only [equivalence₁UnitIso_eq, equivalence₁UnitIso_hom_app, comp_id, id_comp, assoc,
+    equivalence₂UnitIso_hom_app]
   rfl
 
 variable {eB}
diff --git a/Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean b/Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
index d8a661f4056b0..ae05211a3fe1e 100644
--- a/Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
+++ b/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. -/
diff --git a/Mathlib/Analysis/Analytic/OfScalars.lean b/Mathlib/Analysis/Analytic/OfScalars.lean
index 771e16242e8ad..5674b07141092 100644
--- a/Mathlib/Analysis/Analytic/OfScalars.lean
+++ b/Mathlib/Analysis/Analytic/OfScalars.lean
@@ -139,12 +139,12 @@ theorem ofScalarsSum_unop [T2Space E] (x : Eᵐᵒᵖ) :
 
 end Field
 
-section Normed
+section Seminormed
 
 open Filter ENNReal
 open scoped Topology NNReal
 
-variable {𝕜 : Type*} (E : Type*) [NontriviallyNormedField 𝕜] [NormedRing E]
+variable {𝕜 : Type*} (E : Type*) [NontriviallyNormedField 𝕜] [SeminormedRing E]
     [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ)
 
 -- Also works:
@@ -152,7 +152,8 @@ variable {𝕜 : Type*} (E : Type*) [NontriviallyNormedField 𝕜] [NormedRing E
 set_option maxSynthPendingDepth 2 in
 theorem ofScalars_norm_eq_mul :
     ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ := by
-  rw [ofScalars, norm_smul (c n) (ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E)]
+  set_option maxSynthPendingDepth 2 in
+  rw [ofScalars, norm_smul]
 
 theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖ := by
   simp only [ofScalars_norm_eq_mul]
@@ -163,6 +164,16 @@ theorem ofScalars_norm_le (hn : n > 0) : ‖ofScalars E c n‖ ≤ ‖c n‖ :=
 theorem ofScalars_norm [NormOneClass E] : ‖ofScalars E c n‖ = ‖c n‖ := by
   simp [ofScalars_norm_eq_mul]
 
+end Seminormed
+
+section Normed
+
+open Filter ENNReal
+open scoped Topology NNReal
+
+variable {𝕜 : Type*} (E : Type*) [NontriviallyNormedField 𝕜] [NormedRing E]
+    [NormedAlgebra 𝕜 E] (c : ℕ → 𝕜) (n : ℕ)
+
 private theorem tendsto_succ_norm_div_norm {r r' : ℝ≥0} (hr' : r' ≠ 0)
     (hc : Tendsto (fun n ↦ ‖c n.succ‖ / ‖c n‖) atTop (𝓝 r)) :
       Tendsto (fun n ↦ ‖‖c (n + 1)‖ * r' ^ (n + 1)‖ /
diff --git a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
index d0a29face182e..ef49406727787 100644
--- a/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
+++ b/Mathlib/Analysis/Asymptotics/AsymptoticEquivalent.lean
@@ -254,12 +254,29 @@ end SMul
 
 section mul_inv
 
-variable {α β : Type*} [NormedField β] {t u v w : α → β} {l : Filter α}
+variable {α ι β : Type*} [NormedField β] {t u v w : α → β} {l : Filter α}
 
-theorem IsEquivalent.mul (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w :=
+protected theorem IsEquivalent.mul (htu : t ~[l] u) (hvw : v ~[l] w) : t * v ~[l] u * w :=
   htu.smul hvw
 
-theorem IsEquivalent.inv (huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x ↦ (v x)⁻¹ := by
+theorem IsEquivalent.listProd {L : List ι} {f g : ι → α → β} (h : ∀ i ∈ L, f i ~[l] g i) :
+    (fun x ↦ (L.map (f · x)).prod) ~[l] (fun x ↦ (L.map (g · x)).prod) := by
+  induction L with
+  | nil => simp [IsEquivalent.refl]
+  | cons i L ihL =>
+    simp only [List.forall_mem_cons, List.map_cons, List.prod_cons] at h ⊢
+    exact h.1.mul (ihL h.2)
+
+theorem IsEquivalent.multisetProd {s : Multiset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
+    (fun x ↦ (s.map (f · x)).prod) ~[l] (fun x ↦ (s.map (g · x)).prod) := by
+  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
+  exact listProd h
+
+theorem IsEquivalent.finsetProd {s : Finset ι} {f g : ι → α → β} (h : ∀ i ∈ s, f i ~[l] g i) :
+    (∏ i ∈ s, f i ·) ~[l] (∏ i ∈ s, g i ·) :=
+  multisetProd h
+
+protected theorem IsEquivalent.inv (huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x ↦ (v x)⁻¹ := by
   rw [isEquivalent_iff_exists_eq_mul] at *
   rcases huv with ⟨φ, hφ, h⟩
   rw [← inv_one]
@@ -267,7 +284,7 @@ theorem IsEquivalent.inv (huv : u ~[l] v) : (fun x ↦ (u x)⁻¹) ~[l] fun x 
   convert h.inv
   simp [mul_comm]
 
-theorem IsEquivalent.div (htu : t ~[l] u) (hvw : v ~[l] w) :
+protected theorem IsEquivalent.div (htu : t ~[l] u) (hvw : v ~[l] w) :
     (fun x ↦ t x / v x) ~[l] fun x ↦ u x / w x := by
   simpa only [div_eq_mul_inv] using htu.mul hvw.inv
 
diff --git a/Mathlib/Analysis/Asymptotics/Asymptotics.lean b/Mathlib/Analysis/Asymptotics/Asymptotics.lean
index 74755cbeef3a1..b38690a42c515 100644
--- a/Mathlib/Analysis/Asymptotics/Asymptotics.lean
+++ b/Mathlib/Analysis/Asymptotics/Asymptotics.lean
@@ -1570,11 +1570,11 @@ variable {ι : Type*} {A : ι → α → E'} {C : ι → ℝ} {s : Finset ι}
 
 theorem IsBigOWith.sum (h : ∀ i ∈ s, IsBigOWith (C i) l (A i) g) :
     IsBigOWith (∑ i ∈ s, C i) l (fun x => ∑ i ∈ s, A i x) g := by
-  classical
-  induction' s using Finset.induction_on with i s is IH
-  · simp only [isBigOWith_zero', Finset.sum_empty, forall_true_iff]
-  · simp only [is, Finset.sum_insert, not_false_iff]
-    exact (h _ (Finset.mem_insert_self i s)).add (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
+  induction s using Finset.cons_induction with
+  | empty => simp only [isBigOWith_zero', Finset.sum_empty, forall_true_iff]
+  | cons i s is IH =>
+    simp only [is, Finset.sum_cons, Finset.forall_mem_cons] at h ⊢
+    exact h.1.add (IH h.2)
 
 theorem IsBigO.sum (h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x) =O[l] g := by
   simp only [IsBigO_def] at *
@@ -1582,14 +1582,60 @@ theorem IsBigO.sum (h : ∀ i ∈ s, A i =O[l] g) : (fun x => ∑ i ∈ s, A i x
   exact ⟨_, IsBigOWith.sum hC⟩
 
 theorem IsLittleO.sum (h : ∀ i ∈ s, A i =o[l] g') : (fun x => ∑ i ∈ s, A i x) =o[l] g' := by
-  classical
-  induction' s using Finset.induction_on with i s is IH
-  · simp only [isLittleO_zero, Finset.sum_empty, forall_true_iff]
-  · simp only [is, Finset.sum_insert, not_false_iff]
-    exact (h _ (Finset.mem_insert_self i s)).add (IH fun j hj => h _ (Finset.mem_insert_of_mem hj))
+  simp only [← Finset.sum_apply]
+  exact Finset.sum_induction A (· =o[l] g') (fun _ _ ↦ .add) (isLittleO_zero ..) h
 
 end Sum
 
+section Prod
+variable {ι : Type*}
+
+theorem IsBigO.listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜}
+    (hf : ∀ i ∈ L, f i =O[l] g i) :
+    (fun x ↦ (L.map (f · x)).prod) =O[l] (fun x ↦ (L.map (g · x)).prod) := by
+  induction L with
+  | nil => simp [isBoundedUnder_const]
+  | cons i L ihL =>
+    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons] at hf ⊢
+    exact hf.1.mul (ihL hf.2)
+
+theorem IsBigO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
+    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (hf : ∀ i ∈ s, f i =O[l] g i) :
+    (fun x ↦ (s.map (f · x)).prod) =O[l] (fun x ↦ (s.map (g · x)).prod) := by
+  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
+  exact mod_cast IsBigO.listProd hf
+
+theorem IsBigO.finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
+    {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜}
+    (hf : ∀ i ∈ s, f i =O[l] g i) : (∏ i ∈ s, f i ·) =O[l] (∏ i ∈ s, g i ·) :=
+  .multisetProd hf
+
+theorem IsLittleO.listProd {L : List ι} {f : ι → α → R} {g : ι → α → 𝕜}
+    (h₁ : ∀ i ∈ L, f i =O[l] g i) (h₂ : ∃ i ∈ L, f i =o[l] g i) :
+    (fun x ↦ (L.map (f · x)).prod) =o[l] (fun x ↦ (L.map (g · x)).prod) := by
+  induction L with
+  | nil => simp at h₂
+  | cons i L ihL =>
+    simp only [List.map_cons, List.prod_cons, List.forall_mem_cons, List.exists_mem_cons_iff]
+      at h₁ h₂ ⊢
+    cases h₂ with
+    | inl hi => exact hi.mul_isBigO <| .listProd h₁.2
+    | inr hL => exact h₁.1.mul_isLittleO <| ihL h₁.2 hL
+
+theorem IsLittleO.multisetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
+    {s : Multiset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i)
+    (h₂ : ∃ i ∈ s, f i =o[l] g i) :
+    (fun x ↦ (s.map (f · x)).prod) =o[l] (fun x ↦ (s.map (g · x)).prod) := by
+  obtain ⟨l, rfl⟩ : ∃ l : List ι, ↑l = s := Quotient.mk_surjective s
+  exact mod_cast IsLittleO.listProd h₁ h₂
+
+theorem IsLittleO.finsetProd {R 𝕜 : Type*} [SeminormedCommRing R] [NormedField 𝕜]
+    {s : Finset ι} {f : ι → α → R} {g : ι → α → 𝕜} (h₁ : ∀ i ∈ s, f i =O[l] g i)
+    (h₂ : ∃ i ∈ s, f i =o[l] g i) : (∏ i ∈ s, f i ·) =o[l] (∏ i ∈ s, g i ·) :=
+  .multisetProd h₁ h₂
+
+end Prod
+
 /-! ### Relation between `f = o(g)` and `f / g → 0` -/
 
 
diff --git a/Mathlib/Analysis/Asymptotics/Theta.lean b/Mathlib/Analysis/Asymptotics/Theta.lean
index f41f4161c7d45..2ec951024df70 100644
--- a/Mathlib/Analysis/Asymptotics/Theta.lean
+++ b/Mathlib/Analysis/Asymptotics/Theta.lean
@@ -204,6 +204,20 @@ theorem IsTheta.mul {f₁ f₂ : α → 𝕜} {g₁ g₂ : α → 𝕜'} (h₁ :
     (fun x ↦ f₁ x * f₂ x) =Θ[l] fun x ↦ g₁ x * g₂ x :=
   h₁.smul h₂
 
+theorem IsTheta.listProd {ι : Type*} {L : List ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'}
+    (h : ∀ i ∈ L, f i =Θ[l] g i) :
+    (fun x ↦ (L.map (f · x)).prod) =Θ[l] (fun x ↦ (L.map (g · x)).prod) :=
+  ⟨.listProd fun i hi ↦ (h i hi).isBigO, .listProd fun i hi ↦ (h i hi).symm.isBigO⟩
+
+theorem IsTheta.multisetProd {ι : Type*} {s : Multiset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'}
+    (h : ∀ i ∈ s, f i =Θ[l] g i) :
+    (fun x ↦ (s.map (f · x)).prod) =Θ[l] (fun x ↦ (s.map (g · x)).prod) :=
+  ⟨.multisetProd fun i hi ↦ (h i hi).isBigO, .multisetProd fun i hi ↦ (h i hi).symm.isBigO⟩
+
+theorem IsTheta.finsetProd {ι : Type*} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'}
+    (h : ∀ i ∈ s, f i =Θ[l] g i) : (∏ i ∈ s, f i ·) =Θ[l] (∏ i ∈ s, g i ·) :=
+  ⟨.finsetProd fun i hi ↦ (h i hi).isBigO, .finsetProd fun i hi ↦ (h i hi).symm.isBigO⟩
+
 theorem IsTheta.inv {f : α → 𝕜} {g : α → 𝕜'} (h : f =Θ[l] g) :
     (fun x ↦ (f x)⁻¹) =Θ[l] fun x ↦ (g x)⁻¹ :=
   ⟨h.2.inv_rev h.1.eq_zero_imp, h.1.inv_rev h.2.eq_zero_imp⟩
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
index 8e43434bef5ac..3fe783ba69ee2 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
+++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
@@ -155,7 +155,7 @@ section Normal
 
 instance IsStarNormal.instContinuousFunctionalCalculus {A : Type*} [CStarAlgebra A] :
     ContinuousFunctionalCalculus ℂ (IsStarNormal : A → Prop) where
-  predicate_zero := isStarNormal_zero
+  predicate_zero := .zero
   spectrum_nonempty a _ := spectrum.nonempty a
   exists_cfc_of_predicate a ha := by
     refine ⟨(StarAlgebra.elemental ℂ a).subtype.comp <| continuousFunctionalCalculus a,
diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
index ea55c06fddf1e..0cf2fabda7a17 100644
--- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
+++ b/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
 
diff --git a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
index 0ebab41ba1c2a..eb2240b7ca333 100644
--- a/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
+++ b/Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
@@ -106,6 +106,7 @@ structure OrderedFinpartition (n : ℕ) where
   disjoint : PairwiseDisjoint univ fun m ↦ range (emb m)
   /-- The parts cover everything -/
   cover x : ∃ m, x ∈ range (emb m)
+  deriving DecidableEq
 
 namespace OrderedFinpartition
 
diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
index 6c60138a2473d..4a71d1dff9424 100644
--- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
+++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
@@ -785,7 +785,7 @@ end
 
 section
 
-variable {n : ℕ} {A : Type*} [NormedRing A] [NormedAlgebra 𝕜 A]
+variable {n : ℕ} {A : Type*} [SeminormedRing A] [NormedAlgebra 𝕜 A]
 
 theorem norm_mkPiAlgebraFin_succ_le : ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n.succ A‖ ≤ 1 := by
   refine opNorm_le_bound zero_le_one fun m => ?_
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
index 27a9142d793a9..bdb5875943ebe 100644
--- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/ExpLog.lean
+++ b/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]
 
diff --git a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean b/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean
index 487d14cd2871b..0bdd483e3237a 100644
--- a/Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow.lean
+++ b/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)]
diff --git a/Mathlib/Analysis/SpecificLimits/Basic.lean b/Mathlib/Analysis/SpecificLimits/Basic.lean
index c226f8f39d7af..40a14b4c0240c 100644
--- a/Mathlib/Analysis/SpecificLimits/Basic.lean
+++ b/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 `∞`. -/
diff --git a/Mathlib/CategoryTheory/Abelian/Exact.lean b/Mathlib/CategoryTheory/Abelian/Exact.lean
index badc3ad7a0d10..30b6b7aab74df 100644
--- a/Mathlib/CategoryTheory/Abelian/Exact.lean
+++ b/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]
diff --git a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean b/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
index 1473b0ef27413..9110373e9c67a 100644
--- a/Mathlib/CategoryTheory/Abelian/InjectiveResolution.lean
+++ b/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)
diff --git a/Mathlib/CategoryTheory/Action/Limits.lean b/Mathlib/CategoryTheory/Action/Limits.lean
index 00fbf901e87fc..a997429802737 100644
--- a/Mathlib/CategoryTheory/Action/Limits.lean
+++ b/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 :=
diff --git a/Mathlib/CategoryTheory/Action/Monoidal.lean b/Mathlib/CategoryTheory/Action/Monoidal.lean
index 5428444039ef2..98d9b5620c1a2 100644
--- a/Mathlib/CategoryTheory/Action/Monoidal.lean
+++ b/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
diff --git a/Mathlib/CategoryTheory/Adjunction/Basic.lean b/Mathlib/CategoryTheory/Adjunction/Basic.lean
index 9ba41bce3a283..6c4183721f9f5 100644
--- a/Mathlib/CategoryTheory/Adjunction/Basic.lean
+++ b/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
 
@@ -516,12 +516,14 @@ variable {E : Type u₃} [ℰ : Category.{v₃} E] {H : D ⥤ E} {I : E ⥤ D}
 
 See <https://stacks.math.columbia.edu/tag/0DV0>.
 -/
+@[simps! (config := .lemmasOnly) unit counit]
 def comp : F ⋙ H ⊣ I ⋙ G :=
   mk' {
     homEquiv := fun _ _ ↦ Equiv.trans (adj₂.homEquiv _ _) (adj₁.homEquiv _ _)
-    unit := adj₁.unit ≫ (whiskerLeft F <| whiskerRight adj₂.unit G) ≫ (Functor.associator _ _ _).inv
-    counit :=
-      (Functor.associator _ _ _).hom ≫ (whiskerLeft I <| whiskerRight adj₁.counit H) ≫ adj₂.counit }
+    unit := adj₁.unit ≫ whiskerRight (F.rightUnitor.inv ≫ whiskerLeft F adj₂.unit ≫
+      (Functor.associator _ _ _ ).inv) G ≫ (Functor.associator _ _ _).hom
+    counit := (Functor.associator _ _ _ ).inv ≫ whiskerRight ((Functor.associator _ _ _ ).hom ≫
+      whiskerLeft _ adj₁.counit ≫ I.rightUnitor.hom) _ ≫ adj₂.counit }
 
 @[simp, reassoc]
 lemma comp_unit_app (X : C) :
@@ -668,10 +670,10 @@ lemma isLeftAdjoint_inverse : e.inverse.IsLeftAdjoint :=
 lemma isRightAdjoint_functor : e.functor.IsRightAdjoint :=
   e.symm.isRightAdjoint_inverse
 
+lemma refl_toAdjunction : (refl (C := C)).toAdjunction = Adjunction.id := rfl
+
 lemma trans_toAdjunction {E : Type*} [Category E] (e' : D ≌ E) :
-    (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction := by
-  ext
-  simp [trans]
+    (e.trans e').toAdjunction = e.toAdjunction.comp e'.toAdjunction := rfl
 
 end Equivalence
 
diff --git a/Mathlib/CategoryTheory/Adjunction/Mates.lean b/Mathlib/CategoryTheory/Adjunction/Mates.lean
index ca344b3aa3796..cd608363c1820 100644
--- a/Mathlib/CategoryTheory/Adjunction/Mates.lean
+++ b/Mathlib/CategoryTheory/Adjunction/Mates.lean
@@ -208,9 +208,8 @@ theorem mateEquiv_hcomp
       rightAdjointSquare.hcomp (mateEquiv adj₁ adj₂ α) (mateEquiv adj₃ adj₄ β) := by
   unfold leftAdjointSquare.hcomp rightAdjointSquare.hcomp mateEquiv Adjunction.comp
   ext c
-  simp only [comp_obj, mk'_unit, whiskerLeft_comp, whiskerLeft_twice, mk'_counit, whiskerRight_comp,
-    assoc, Equiv.coe_fn_mk, comp_app, whiskerLeft_app, whiskerRight_app, id_obj, associator_inv_app,
-    Functor.comp_map, associator_hom_app, map_id, id_comp, whiskerRight_twice]
+  dsimp
+  simp only [comp_id, map_comp, id_comp, assoc]
   slice_rhs 2 4 =>
     rw [← R₂.map_comp, ← R₂.map_comp, ← assoc, ← unit_naturality (adj₄)]
   rw [R₂.map_comp, L₄.map_comp, R₄.map_comp, R₂.map_comp]
diff --git a/Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean b/Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean
index 02482d12bfd09..a0058e9be01b0 100644
--- a/Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean
+++ b/Mathlib/CategoryTheory/Bicategory/FunctorBicategory/Oplax.lean
@@ -50,19 +50,19 @@ def whiskerRight {η θ : F ⟶ G} (Γ : η ⟶ θ) (ι : G ⟶ H) : η ≫ ι 
 -- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
 @[simps!]
 def associator (η : F ⟶ G) (θ : G ⟶ H) (ι : H ⟶ I) : (η ≫ θ) ≫ ι ≅ η ≫ θ ≫ ι :=
-  ModificationIso.ofComponents (fun a => α_ (η.app a) (θ.app a) (ι.app a)) (by aesop_cat)
+  ModificationIso.ofComponents (fun a => α_ (η.app a) (θ.app a) (ι.app a)) (by simp)
 
 /-- Left unitor for the vertical composition of oplax natural transformations. -/
 -- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
 @[simps!]
 def leftUnitor (η : F ⟶ G) : 𝟙 F ≫ η ≅ η :=
-  ModificationIso.ofComponents (fun a => λ_ (η.app a)) (by aesop_cat)
+  ModificationIso.ofComponents (fun a => λ_ (η.app a)) (by simp)
 
 /-- Right unitor for the vertical composition of oplax natural transformations. -/
 -- Porting note: verified that projections are correct and changed @[simps] to @[simps!]
 @[simps!]
 def rightUnitor (η : F ⟶ G) : η ≫ 𝟙 G ≅ η :=
-  ModificationIso.ofComponents (fun a => ρ_ (η.app a)) (by aesop_cat)
+  ModificationIso.ofComponents (fun a => ρ_ (η.app a)) (by simp)
 
 end OplaxNatTrans
 
diff --git a/Mathlib/CategoryTheory/Category/Cat.lean b/Mathlib/CategoryTheory/Category/Cat.lean
index 7d16c775e8b1d..b76adff0b2f61 100644
--- a/Mathlib/CategoryTheory/Category/Cat.lean
+++ b/Mathlib/CategoryTheory/Category/Cat.lean
@@ -182,7 +182,7 @@ def typeToCat : Type u ⥤ Cat where
       simp only [id_eq, eqToHom_refl, Cat.id_map, Category.comp_id, Category.id_comp]
       apply ULift.ext
       aesop_cat
-    · aesop_cat
+    · simp
   map_comp f g := by apply Functor.ext; aesop_cat
 
 instance : Functor.Faithful typeToCat.{u} where
diff --git a/Mathlib/CategoryTheory/Category/Cat/Limit.lean b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
index e16a6957e1e3f..ae7ce8e214d0b 100644
--- a/Mathlib/CategoryTheory/Category/Cat/Limit.lean
+++ b/Mathlib/CategoryTheory/Category/Cat/Limit.lean
@@ -67,10 +67,10 @@ instance (F : J ⥤ Cat.{v, v}) : Category (limit (F ⋙ Cat.objects)) where
         ← congr_fun (limit.w (homDiagram Y Z) h) g]
   id_comp _ := by
     apply Types.limit_ext.{v, v}
-    aesop_cat
+    simp
   comp_id _ := by
     apply Types.limit_ext.{v, v}
-    aesop_cat
+    simp
 
 /-- Auxiliary definition: the limit category. -/
 @[simps]
diff --git a/Mathlib/CategoryTheory/Comma/Arrow.lean b/Mathlib/CategoryTheory/Comma/Arrow.lean
index cc6d53e196a94..6a161770de191 100644
--- a/Mathlib/CategoryTheory/Comma/Arrow.lean
+++ b/Mathlib/CategoryTheory/Comma/Arrow.lean
@@ -94,15 +94,16 @@ instance {X Y : T} : CoeOut (X ⟶ Y) (Arrow T) where
 /-- A morphism in the arrow category is a commutative square connecting two objects of the arrow
     category. -/
 @[simps]
-def homMk {f g : Arrow T} {u : f.left ⟶ g.left} {v : f.right ⟶ g.right}
-    (w : u ≫ g.hom = f.hom ≫ v) : f ⟶ g where
+def homMk {f g : Arrow T} (u : f.left ⟶ g.left) (v : f.right ⟶ g.right)
+    (w : u ≫ g.hom = f.hom ≫ v := by aesop_cat) : f ⟶ g where
   left := u
   right := v
   w := w
 
 /-- We can also build a morphism in the arrow category out of any commutative square in `T`. -/
 @[simps]
-def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} {u : X ⟶ P} {v : Y ⟶ Q} (w : u ≫ g = f ≫ v) :
+def homMk' {X Y : T} {f : X ⟶ Y} {P Q : T} {g : P ⟶ Q} (u : X ⟶ P) (v : Y ⟶ Q)
+    (w : u ≫ g = f ≫ v := by aesop_cat) :
     Arrow.mk f ⟶ Arrow.mk g where
   left := u
   right := v
diff --git a/Mathlib/CategoryTheory/Comma/Basic.lean b/Mathlib/CategoryTheory/Comma/Basic.lean
index ccbfebe05bd1b..ee0bc05acbe47 100644
--- a/Mathlib/CategoryTheory/Comma/Basic.lean
+++ b/Mathlib/CategoryTheory/Comma/Basic.lean
@@ -289,7 +289,7 @@ theorem map_fst : map α β ⋙ fst L' R' = fst L R ⋙ F₁ :=
 where `α : F₁ ⋙ L' ⟶ L ⋙ F`. -/
 @[simps!]
 def mapFst : map α β ⋙ fst L' R' ≅ fst L R ⋙ F₁ :=
-  NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
+  NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
 
 /-- The equality between `map α β ⋙ snd L' R'` and `snd L R ⋙ F₂`,
 where `β : R ⋙ F ⟶ F₂ ⋙ R'`. -/
@@ -301,7 +301,7 @@ theorem map_snd : map α β ⋙ snd L' R' = snd L R ⋙ F₂ :=
 where `β : R ⋙ F ⟶ F₂ ⋙ R'`. -/
 @[simps!]
 def mapSnd : map α β ⋙ snd L' R' ≅ snd L R ⋙ F₂ :=
-  NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)
+  NatIso.ofComponents (fun _ => Iso.refl _) (by simp)
 
 end
 
diff --git a/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean b/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
index 56df6eace290c..94aa947d47cc9 100644
--- a/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
+++ b/Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@@ -190,7 +190,7 @@ lemma yonedaArrow_val {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj
 /-- If `η` is also `yoneda`-costructured, then `OverArrows η s` is just morphisms of costructured
     arrows. -/
 def costructuredArrowIso (s t : CostructuredArrow yoneda A) : OverArrows s.hom t.hom ≅ t ⟶ s where
-  hom p := CostructuredArrow.homMk p.val (by aesop_cat)
+  hom p := CostructuredArrow.homMk p.val (by simp)
   inv f := yonedaArrow f.left f.w
 
 end OverArrows
@@ -436,7 +436,7 @@ lemma app_unitForward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : Cᵒᵖ)
 /-- Backward direction of the unit. -/
 def unitBackward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) :
     F.obj (op X) → YonedaCollection (restrictedYonedaObj η) X :=
-  fun x => YonedaCollection.mk (yonedaEquiv.symm (η.app _ x)) ⟨x, ⟨by aesop_cat⟩⟩
+  fun x => YonedaCollection.mk (yonedaEquiv.symm (η.app _ x)) ⟨x, ⟨by simp⟩⟩
 
 lemma unitForward_unitBackward {F : Cᵒᵖ ⥤ Type v} (η : F ⟶ A) (X : C) :
     unitForward η X ∘ unitBackward η X = id :=
@@ -513,7 +513,7 @@ lemma counitForward_naturality₂ (s t : (CostructuredArrow yoneda A)ᵒᵖ) (f
   have : (CostructuredArrow.mkPrecomp t.unop.hom f.unop.left).op =
       f ≫ eqToHom (by simp [← CostructuredArrow.eq_mk]) := by
     apply Quiver.Hom.unop_inj
-    aesop_cat
+    simp
   aesop_cat
 
 /-- Backward direction of the counit. -/
diff --git a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
index 22de055a81308..42ce3a6553dbd 100644
--- a/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
+++ b/Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
@@ -126,7 +126,7 @@ lemma homMk'_id (f : StructuredArrow S T) : homMk' f (𝟙 f.right) = eqToHom (b
   ext
   simp [eqToHom_right]
 
-lemma homMk'_mk_id (f : S ⟶ T.obj Y) : homMk' (mk f) (𝟙 Y) = eqToHom (by aesop_cat) :=
+lemma homMk'_mk_id (f : S ⟶ T.obj Y) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
   homMk'_id _
 
 lemma homMk'_comp (f : StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') :
@@ -144,10 +144,10 @@ def mkPostcomp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') : mk f ⟶ mk (f ≫ T.map g)
   left := 𝟙 _
   right := g
 
-lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat
+lemma mkPostcomp_id (f : S ⟶ T.obj Y) : mkPostcomp f (𝟙 Y) = eqToHom (by simp) := by simp
 lemma mkPostcomp_comp (f : S ⟶ T.obj Y) (g : Y ⟶ Y') (g' : Y' ⟶ Y'') :
     mkPostcomp f (g ≫ g') = mkPostcomp f g ≫ mkPostcomp (f ≫ T.map g) g' ≫ eqToHom (by simp) := by
-  aesop_cat
+  simp
 
 /-- To construct an isomorphism of structured arrows,
 we need an isomorphism of the objects underlying the target,
@@ -257,7 +257,7 @@ noncomputable def mkIdInitial [T.Full] [T.Faithful] : IsInitial (mk (𝟙 (T.obj
   desc c := homMk (T.preimage c.pt.hom)
   uniq c m _ := by
     apply CommaMorphism.ext
-    · aesop_cat
+    · simp
     · apply T.map_injective
       simpa only [homMk_right, T.map_preimage, ← w m] using (Category.id_comp _).symm
 
@@ -293,7 +293,7 @@ instance (S : C) (F : B ⥤ C) (G : C ⥤ D) : (post S F G).Faithful where
   map_injective {_ _} _ _ h := by simpa [ext_iff] using h
 
 instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Faithful] : (post S F G).Full where
-  map_surjective f := ⟨homMk f.right (G.map_injective (by simpa using f.w.symm)), by aesop_cat⟩
+  map_surjective f := ⟨homMk f.right (G.map_injective (by simpa using f.w.symm)), by simp⟩
 
 instance (S : C) (F : B ⥤ C) (G : C ⥤ D) [G.Full] : (post S F G).EssSurj where
   mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩
@@ -468,7 +468,7 @@ lemma homMk'_id (f : CostructuredArrow S T) : homMk' f (𝟙 f.left) = eqToHom (
   ext
   simp [eqToHom_left]
 
-lemma homMk'_mk_id (f : S.obj Y ⟶ T) : homMk' (mk f) (𝟙 Y) = eqToHom (by aesop_cat) :=
+lemma homMk'_mk_id (f : S.obj Y ⟶ T) : homMk' (mk f) (𝟙 Y) = eqToHom (by simp) :=
   homMk'_id _
 
 lemma homMk'_comp (f : CostructuredArrow S T) (g : Y' ⟶ f.left) (g' : Y'' ⟶ Y') :
@@ -486,10 +486,10 @@ def mkPrecomp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mk (S.map g ≫ f) ⟶ mk f w
   left := g
   right := 𝟙 _
 
-lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by aesop_cat) := by aesop_cat
+lemma mkPrecomp_id (f : S.obj Y ⟶ T) : mkPrecomp f (𝟙 Y) = eqToHom (by simp) := by simp
 lemma mkPrecomp_comp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) (g' : Y'' ⟶ Y') :
     mkPrecomp f (g' ≫ g) = eqToHom (by simp) ≫ mkPrecomp (S.map g ≫ f) g' ≫ mkPrecomp f g := by
-  aesop_cat
+  simp
 
 /-- To construct an isomorphism of costructured arrows,
 we need an isomorphism of the objects underlying the source,
@@ -634,7 +634,7 @@ instance (F : B ⥤ C) (G : C ⥤ D) (S : C) : (post F G S).Faithful where
   map_injective {_ _} _ _ h := by simpa [ext_iff] using h
 
 instance (F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Faithful] : (post F G S).Full where
-  map_surjective f := ⟨homMk f.left (G.map_injective (by simpa using f.w)), by aesop_cat⟩
+  map_surjective f := ⟨homMk f.left (G.map_injective (by simpa using f.w)), by simp⟩
 
 instance (F : B ⥤ C) (G : C ⥤ D) (S : C) [G.Full] : (post F G S).EssSurj where
   mem_essImage h := ⟨mk (G.preimage h.hom), ⟨isoMk (Iso.refl _) (by simp)⟩⟩
diff --git a/Mathlib/CategoryTheory/DiscreteCategory.lean b/Mathlib/CategoryTheory/DiscreteCategory.lean
index 1d28f0410aa9e..4505a8e1b9584 100644
--- a/Mathlib/CategoryTheory/DiscreteCategory.lean
+++ b/Mathlib/CategoryTheory/DiscreteCategory.lean
@@ -246,9 +246,9 @@ def equivalence {I : Type u₁} {J : Type u₂} (e : I ≃ J) : Discrete I ≌ D
   functor := Discrete.functor (Discrete.mk ∘ (e : I → J))
   inverse := Discrete.functor (Discrete.mk ∘ (e.symm : J → I))
   unitIso :=
-    Discrete.natIso fun i => eqToIso (by aesop_cat)
+    Discrete.natIso fun i => eqToIso (by simp)
   counitIso :=
-    Discrete.natIso fun j => eqToIso (by aesop_cat)
+    Discrete.natIso fun j => eqToIso (by simp)
 
 /-- We can convert an equivalence of `discrete` categories to a type-level `Equiv`. -/
 @[simps]
diff --git a/Mathlib/CategoryTheory/Elements.lean b/Mathlib/CategoryTheory/Elements.lean
index 7d85416b30755..01aa8d0ac97b7 100644
--- a/Mathlib/CategoryTheory/Elements.lean
+++ b/Mathlib/CategoryTheory/Elements.lean
@@ -59,7 +59,7 @@ lemma Functor.Elements.ext {F : C ⥤ Type w} (x y : F.Elements) (h₁ : x.fst =
  -/
 instance categoryOfElements (F : C ⥤ Type w) : Category.{v} F.Elements where
   Hom p q := { f : p.1 ⟶ q.1 // (F.map f) p.2 = q.2 }
-  id p := ⟨𝟙 p.1, by aesop_cat⟩
+  id p := ⟨𝟙 p.1, by simp⟩
   comp {X Y Z} f g := ⟨f.val ≫ g.val, by simp [f.2, g.2]⟩
 
 /-- Natural transformations are mapped to functors between category of elements -/
diff --git a/Mathlib/CategoryTheory/Equivalence.lean b/Mathlib/CategoryTheory/Equivalence.lean
index f6f45ef4bd954..a7842ed6f55b9 100644
--- a/Mathlib/CategoryTheory/Equivalence.lean
+++ b/Mathlib/CategoryTheory/Equivalence.lean
@@ -269,20 +269,19 @@ variable {E : Type u₃} [Category.{v₃} E]
 def trans (e : C ≌ D) (f : D ≌ E) : C ≌ E where
   functor := e.functor ⋙ f.functor
   inverse := f.inverse ⋙ e.inverse
-  unitIso := by
-    refine Iso.trans e.unitIso ?_
-    exact isoWhiskerLeft e.functor (isoWhiskerRight f.unitIso e.inverse)
-  counitIso := by
-    refine Iso.trans ?_ f.counitIso
-    exact isoWhiskerLeft f.inverse (isoWhiskerRight e.counitIso f.functor)
+  unitIso := e.unitIso ≪≫ isoWhiskerRight (e.functor.rightUnitor.symm ≪≫
+    isoWhiskerLeft _ f.unitIso ≪≫ (Functor.associator _ _ _ ).symm) _ ≪≫ Functor.associator _ _ _
+  counitIso := (Functor.associator _ _ _ ).symm ≪≫ isoWhiskerRight ((Functor.associator _ _ _ ) ≪≫
+      isoWhiskerLeft _ e.counitIso ≪≫ f.inverse.rightUnitor) _ ≪≫ f.counitIso
   -- We wouldn't have needed to give this proof if we'd used `Equivalence.mk`,
   -- but we choose to avoid using that here, for the sake of good structure projection `simp`
   -- lemmas.
   functor_unitIso_comp X := by
     dsimp
-    rw [← f.functor.map_comp_assoc, e.functor.map_comp, ← counitInv_app_functor, fun_inv_map,
-      Iso.inv_hom_id_app_assoc, assoc, Iso.inv_hom_id_app, counit_app_functor, ← Functor.map_comp]
-    erw [comp_id, Iso.hom_inv_id_app, Functor.map_id]
+    simp only [comp_id, id_comp, map_comp, fun_inv_map, comp_obj, id_obj, counitInv,
+      functor_unit_comp_assoc, assoc]
+    slice_lhs 2 3 => rw [← Functor.map_comp, Iso.inv_hom_id_app]
+    simp
 
 /-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
 functor. -/
@@ -293,13 +292,13 @@ def funInvIdAssoc (e : C ≌ D) (F : C ⥤ E) : e.functor ⋙ e.inverse ⋙ F 
 theorem funInvIdAssoc_hom_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
     (funInvIdAssoc e F).hom.app X = F.map (e.unitInv.app X) := by
   dsimp [funInvIdAssoc]
-  aesop_cat
+  simp
 
 @[simp]
 theorem funInvIdAssoc_inv_app (e : C ≌ D) (F : C ⥤ E) (X : C) :
     (funInvIdAssoc e F).inv.app X = F.map (e.unit.app X) := by
   dsimp [funInvIdAssoc]
-  aesop_cat
+  simp
 
 /-- Composing a functor with both functors of an equivalence yields a naturally isomorphic
 functor. -/
@@ -310,13 +309,13 @@ def invFunIdAssoc (e : C ≌ D) (F : D ⥤ E) : e.inverse ⋙ e.functor ⋙ F 
 theorem invFunIdAssoc_hom_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
     (invFunIdAssoc e F).hom.app X = F.map (e.counit.app X) := by
   dsimp [invFunIdAssoc]
-  aesop_cat
+  simp
 
 @[simp]
 theorem invFunIdAssoc_inv_app (e : C ≌ D) (F : D ⥤ E) (X : D) :
     (invFunIdAssoc e F).inv.app X = F.map (e.counitInv.app X) := by
   dsimp [invFunIdAssoc]
-  aesop_cat
+  simp
 
 /-- If `C` is equivalent to `D`, then `C ⥤ E` is equivalent to `D ⥤ E`. -/
 @[simps! functor inverse unitIso counitIso]
@@ -525,7 +524,7 @@ i.e. faithful, full, and essentially surjective. -/
 noncomputable def inv (F : C ⥤ D) [F.IsEquivalence] : D ⥤ C where
   obj X := F.objPreimage X
   map {X Y} f := F.preimage ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
-  map_id X := by apply F.map_injective; aesop_cat
+  map_id X := by apply F.map_injective; simp
   map_comp {X Y Z} f g := by apply F.map_injective; simp
 
 /-- Interpret a functor that is an equivalence as an equivalence.
diff --git a/Mathlib/CategoryTheory/Functor/Const.lean b/Mathlib/CategoryTheory/Functor/Const.lean
index ba2d6a7b37e98..63504ca0530c7 100644
--- a/Mathlib/CategoryTheory/Functor/Const.lean
+++ b/Mathlib/CategoryTheory/Functor/Const.lean
@@ -96,7 +96,7 @@ instance [Nonempty J] : Faithful (const J : C ⥤ J ⥤ C) where
 def compConstIso (F : C ⥤ D) :
     F ⋙ Functor.const J ≅ Functor.const J ⋙ (whiskeringRight J C D).obj F :=
   NatIso.ofComponents
-    (fun X => NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
+    (fun X => NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
     (by aesop_cat)
 
 /-- The canonical isomorphism
diff --git a/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean b/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
index 8acc96f8e2d2d..c815ff3015b16 100644
--- a/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
+++ b/Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
@@ -117,7 +117,7 @@ lemma rightDerivedNatTrans_app (τ : F ⟶ F') (X : C) :
 @[simp]
 lemma rightDerivedNatTrans_id :
     rightDerivedNatTrans RF RF α α W (𝟙 F) = 𝟙 RF :=
-  rightDerived_ext RF α W _ _ _ (by aesop_cat)
+  rightDerived_ext RF α W _ _ _ (by simp)
 
 variable [RF'.IsRightDerivedFunctor α' W]
 
@@ -125,7 +125,7 @@ variable [RF'.IsRightDerivedFunctor α' W]
 lemma rightDerivedNatTrans_comp (τ : F ⟶ F') (τ' : F' ⟶ F'') :
     rightDerivedNatTrans RF RF' α α' W τ ≫ rightDerivedNatTrans RF' RF'' α' α'' W τ' =
     rightDerivedNatTrans RF RF'' α α'' W (τ ≫ τ') :=
-  rightDerived_ext RF α W _ _ _ (by aesop_cat)
+  rightDerived_ext RF α W _ _ _ (by simp)
 
 /-- The natural isomorphism `RF ≅ RF'` on right derived functors that is
 induced by a natural isomorphism `F ≅ F'`. -/
diff --git a/Mathlib/CategoryTheory/Functor/FunctorHom.lean b/Mathlib/CategoryTheory/Functor/FunctorHom.lean
index 3f4312c687eaa..be91d1395df1e 100644
--- a/Mathlib/CategoryTheory/Functor/FunctorHom.lean
+++ b/Mathlib/CategoryTheory/Functor/FunctorHom.lean
@@ -131,7 +131,7 @@ def functorHomEquiv (A : C ⥤ Type max u v v') : (A ⟶ F.functorHom G) ≃ Hom
     ext X a Y f
     exact (HomObj.congr_app (congr_fun (φ.naturality f) a) Y (𝟙 _)).trans
       (congr_arg ((φ.app X a).app Y) (by simp))
-  right_inv x := by aesop
+  right_inv x := by simp
 
 variable {F G} in
 /-- Morphisms `(𝟙_ (C ⥤ Type max v' v u) ⟶ F.functorHom G)` are in bijection with
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
index 4ea68229bb26b..b969b1f888ff4 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Basic.lean
@@ -102,7 +102,7 @@ noncomputable def homEquivOfIsRightKanExtension (G : D ⥤ H) :
     (G ⟶ F') ≃ (L ⋙ G ⟶ F) where
   toFun β := whiskerLeft _ β ≫ α
   invFun β := liftOfIsRightKanExtension _ α _ β
-  left_inv β := Functor.hom_ext_of_isRightKanExtension _ α _ _ (by aesop_cat)
+  left_inv β := Functor.hom_ext_of_isRightKanExtension _ α _ _ (by simp)
   right_inv := by aesop_cat
 
 lemma isRightKanExtension_of_iso {F' F'' : D ⥤ H} (e : F' ≅ F'') {L : C ⥤ D} {F : C ⥤ H}
@@ -193,7 +193,7 @@ noncomputable def homEquivOfIsLeftKanExtension (G : D ⥤ H) :
     (F' ⟶ G) ≃ (F ⟶ L ⋙ G) where
   toFun β := α ≫ whiskerLeft _ β
   invFun β := descOfIsLeftKanExtension _ α _ β
-  left_inv β := Functor.hom_ext_of_isLeftKanExtension _ α _ _ (by aesop_cat)
+  left_inv β := Functor.hom_ext_of_isLeftKanExtension _ α _ _ (by simp)
   right_inv := by aesop_cat
 
 lemma isLeftKanExtension_of_iso {F' : D ⥤ H} {F'' : D ⥤ H} (e : F' ≅ F'')
diff --git a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
index a1a044d1a3846..12c6638bcdfe2 100644
--- a/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
+++ b/Mathlib/CategoryTheory/Functor/KanExtension/Pointwise.lean
@@ -140,8 +140,8 @@ def isPointwiseLeftKanExtensionEquivOfIso (e : E ≅ E') :
     E.IsPointwiseLeftKanExtension ≃ E'.IsPointwiseLeftKanExtension where
   toFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y) (h Y)
   invFun h := fun Y => (isPointwiseLeftKanExtensionAtEquivOfIso e Y).symm (h Y)
-  left_inv h := by aesop
-  right_inv h := by aesop
+  left_inv h := by simp
+  right_inv h := by simp
 
 variable (h : E.IsPointwiseLeftKanExtension)
 include h
@@ -277,8 +277,8 @@ def isPointwiseRightKanExtensionEquivOfIso (e : E ≅ E') :
     E.IsPointwiseRightKanExtension ≃ E'.IsPointwiseRightKanExtension where
   toFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y) (h Y)
   invFun h := fun Y => (isPointwiseRightKanExtensionAtEquivOfIso e Y).symm (h Y)
-  left_inv h := by aesop
-  right_inv h := by aesop
+  left_inv h := by simp
+  right_inv h := by simp
 
 variable (h : E.IsPointwiseRightKanExtension)
 include h
diff --git a/Mathlib/CategoryTheory/Galois/Decomposition.lean b/Mathlib/CategoryTheory/Galois/Decomposition.lean
index 0266fabf8bc16..37f5ba335107f 100644
--- a/Mathlib/CategoryTheory/Galois/Decomposition.lean
+++ b/Mathlib/CategoryTheory/Galois/Decomposition.lean
@@ -66,7 +66,7 @@ private lemma has_decomp_connected_components_aux_initial (X : C) (h : IsInitial
     ∃ (ι : Type) (f : ι → C) (g : (i : ι) → (f i) ⟶ X) (_ : IsColimit (Cofan.mk X g)),
     (∀ i, IsConnected (f i)) ∧ Finite ι := by
   refine ⟨Empty, fun _ ↦ X, fun _ ↦ 𝟙 X, ?_⟩
-  use mkCofanColimit _ (fun s ↦ IsInitial.to h s.pt) (fun s ↦ by aesop)
+  use mkCofanColimit _ (fun s ↦ IsInitial.to h s.pt) (fun s ↦ by simp)
     (fun s m _ ↦ IsInitial.hom_ext h m _)
   exact ⟨by simp only [IsEmpty.forall_iff], inferInstance⟩
 
diff --git a/Mathlib/CategoryTheory/GlueData.lean b/Mathlib/CategoryTheory/GlueData.lean
index 2c0b603d6f43f..fcea852442c19 100644
--- a/Mathlib/CategoryTheory/GlueData.lean
+++ b/Mathlib/CategoryTheory/GlueData.lean
@@ -443,9 +443,9 @@ def GlueData'.t'' (D : GlueData' C) (i j k : D.J) :
   else
     haveI := Ne.symm hij
     pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by rw [dif_neg hik]))
-        (eqToHom (by aesop)) (by delta f'; aesop) (by delta f'; aesop) ≫
+        (eqToHom (by simp)) (by delta f'; aesop) (by delta f'; aesop) ≫
       D.t' i j k hij hik hjk ≫
-      pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by aesop)) (eqToHom (by aesop))
+      pullback.map _ _ _ _ (eqToHom (by aesop)) (eqToHom (by aesop)) (eqToHom (by simp))
         (by delta f'; aesop) (by delta f'; aesop)
 
 open scoped Classical in
diff --git a/Mathlib/CategoryTheory/GradedObject/Single.lean b/Mathlib/CategoryTheory/GradedObject/Single.lean
index 180a200b1ed92..e5add88c366ef 100644
--- a/Mathlib/CategoryTheory/GradedObject/Single.lean
+++ b/Mathlib/CategoryTheory/GradedObject/Single.lean
@@ -77,7 +77,7 @@ variable (C) in
 evaluation functor `eval j` identifies to the identity functor. -/
 @[simps!]
 noncomputable def singleCompEval (j : J) : single j ⋙ eval j ≅ 𝟭 C :=
-  NatIso.ofComponents (singleObjApplyIso j) (by aesop_cat)
+  NatIso.ofComponents (singleObjApplyIso j) (by simp)
 
 end GradedObject
 
diff --git a/Mathlib/CategoryTheory/Groupoid.lean b/Mathlib/CategoryTheory/Groupoid.lean
index a880d7c21b5a3..5b43b7b7a2a4b 100644
--- a/Mathlib/CategoryTheory/Groupoid.lean
+++ b/Mathlib/CategoryTheory/Groupoid.lean
@@ -95,7 +95,7 @@ variable (X Y)
 /-- In a groupoid, isomorphisms are equivalent to morphisms. -/
 def Groupoid.isoEquivHom : (X ≅ Y) ≃ (X ⟶ Y) where
   toFun := Iso.hom
-  invFun f := ⟨f, Groupoid.inv f, (by aesop_cat), (by aesop_cat)⟩
+  invFun f := ⟨f, Groupoid.inv f, (by simp), (by simp)⟩
   left_inv _ := Iso.ext rfl
   right_inv _ := rfl
 
diff --git a/Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean b/Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
index e227d08f5cbc7..8c6c94626e7a8 100644
--- a/Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
+++ b/Mathlib/CategoryTheory/Idempotents/FunctorExtension.lean
@@ -103,7 +103,7 @@ def functorExtension₁CompWhiskeringLeftToKaroubiIso :
       (fun X =>
         { hom := { f := (F.obj X).p }
           inv := { f := (F.obj X).p } })
-      (fun {X Y} f => by aesop_cat))
+      (fun {X Y} f => by simp))
     (by aesop_cat)
 
 /-- The counit isomorphism of the equivalence `(C ⥤ Karoubi D) ≌ (Karoubi C ⥤ Karoubi D)`. -/
@@ -180,7 +180,7 @@ def functorExtension₂CompWhiskeringLeftToKaroubiIso :
       (fun X =>
         { hom := { f := 𝟙 _ }
           inv := { f := 𝟙 _ } })
-      (by aesop_cat))
+      (by simp))
     (by aesop_cat)
 
 section IsIdempotentComplete
diff --git a/Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean b/Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean
index 52ef588b3f18e..3efddee1016cd 100644
--- a/Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean
+++ b/Mathlib/CategoryTheory/Idempotents/HomologicalComplex.lean
@@ -120,7 +120,7 @@ def inverse : HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C
 `Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c`. -/
 @[simps!]
 def counitIso : inverse ⋙ functor ≅ 𝟭 (HomologicalComplex (Karoubi C) c) :=
-  eqToIso (Functor.ext (fun P => HomologicalComplex.ext (by aesop_cat) (by aesop_cat))
+  eqToIso (Functor.ext (fun P => HomologicalComplex.ext (by aesop_cat) (by simp))
     (by aesop_cat))
 
 /-- The unit isomorphism of the equivalence
diff --git a/Mathlib/CategoryTheory/Idempotents/Karoubi.lean b/Mathlib/CategoryTheory/Idempotents/Karoubi.lean
index d4b4fc8a4f69e..aa8ebd6d96a7d 100644
--- a/Mathlib/CategoryTheory/Idempotents/Karoubi.lean
+++ b/Mathlib/CategoryTheory/Idempotents/Karoubi.lean
@@ -273,11 +273,11 @@ theorem decompId_p_toKaroubi (X : C) : decompId_p ((toKaroubi C).obj X) = 𝟙 _
 
 theorem decompId_i_naturality {P Q : Karoubi C} (f : P ⟶ Q) :
     f ≫ decompId_i Q = decompId_i P ≫ (by exact Hom.mk f.f (by simp)) := by
-  aesop_cat
+  simp
 
 theorem decompId_p_naturality {P Q : Karoubi C} (f : P ⟶ Q) :
     decompId_p P ≫ f = (by exact Hom.mk f.f (by simp)) ≫ decompId_p Q := by
-  aesop_cat
+  simp
 
 @[simp]
 theorem zsmul_hom [Preadditive C] {P Q : Karoubi C} (n : ℤ) (f : P ⟶ Q) : (n • f).f = n • f.f :=
diff --git a/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean b/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
index 2fc3351f029a2..4195b5218d23f 100644
--- a/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
+++ b/Mathlib/CategoryTheory/Idempotents/KaroubiKaroubi.lean
@@ -46,7 +46,7 @@ instance [Preadditive C] : Functor.Additive (inverse C) where
 /-- The unit isomorphism of the equivalence -/
 @[simps!]
 def unitIso : 𝟭 (Karoubi C) ≅ toKaroubi (Karoubi C) ⋙ inverse C :=
-  eqToIso (Functor.ext (by aesop_cat) (by aesop_cat))
+  eqToIso (Functor.ext (by aesop_cat) (by simp))
 
 attribute [local simp] p_comm_f in
 /-- The counit isomorphism of the equivalence -/
diff --git a/Mathlib/CategoryTheory/IsConnected.lean b/Mathlib/CategoryTheory/IsConnected.lean
index 73adc542b3de7..9f27285ea78dc 100644
--- a/Mathlib/CategoryTheory/IsConnected.lean
+++ b/Mathlib/CategoryTheory/IsConnected.lean
@@ -102,7 +102,7 @@ def isoConstant [IsPreconnected J] {α : Type u₂} (F : J ⥤ Discrete α) (j :
     F ≅ (Functor.const J).obj (F.obj j) :=
   (IsPreconnected.IsoConstantAux.factorThroughDiscrete F).symm
     ≪≫ isoWhiskerRight (IsPreconnected.iso_constant _ j).some _
-    ≪≫ NatIso.ofComponents (fun _ => eqToIso Function.apply_invFun_apply) (by aesop_cat)
+    ≪≫ NatIso.ofComponents (fun _ => eqToIso Function.apply_invFun_apply) (by simp)
 
 /-- If `J` is connected, any functor to a discrete category is constant on objects.
 The converse is given in `IsConnected.of_any_functor_const_on_obj`.
diff --git a/Mathlib/CategoryTheory/Limits/Cones.lean b/Mathlib/CategoryTheory/Limits/Cones.lean
index 6fee46c53e64c..68bb5355b5bfe 100644
--- a/Mathlib/CategoryTheory/Limits/Cones.lean
+++ b/Mathlib/CategoryTheory/Limits/Cones.lean
@@ -158,7 +158,7 @@ instance inhabitedCocone (F : Discrete PUnit ⥤ C) : Inhabited (Cocone F) :=
               intro X Y f
               match X, Y, f with
               | .mk A, .mk B, .up g =>
-                aesop_cat
+                simp
            }
   }⟩
 
@@ -408,7 +408,7 @@ def functoriality : Cone F ⥤ Cone (F ⋙ G) where
     { pt := G.obj A.pt
       π :=
         { app := fun j => G.map (A.π.app j)
-          naturality := by intros; erw [← G.map_comp]; aesop_cat } }
+          naturality := by intros; erw [← G.map_comp]; simp } }
   map f :=
     { hom := G.map f.hom
       w := fun j => by simp [-ConeMorphism.w, ← f.w j] }
@@ -606,7 +606,7 @@ def functoriality : Cocone F ⥤ Cocone (F ⋙ G) where
     { pt := G.obj A.pt
       ι :=
         { app := fun j => G.map (A.ι.app j)
-          naturality := by intros; erw [← G.map_comp]; aesop_cat } }
+          naturality := by intros; erw [← G.map_comp]; simp } }
   map f :=
     { hom := G.map f.hom
       w := by intros; rw [← Functor.map_comp, CoconeMorphism.w] }
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean b/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
index 5712931af86a2..12841a497aa58 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
+++ b/Mathlib/CategoryTheory/Limits/Constructions/Filtered.lean
@@ -68,7 +68,7 @@ def liftToFinsetColimitCocone [HasColimitsOfShape (Finset (Discrete α)) C]
         convert h j using 1
         · simp [← colimit.w (liftToFinsetObj F) ⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩]
           rfl
-        · aesop_cat }
+        · simp }
 
 variable (C) (α)
 
@@ -180,7 +180,7 @@ def liftToFinsetLimitCone [HasLimitsOfShape (Finset (Discrete α))ᵒᵖ C]
         convert h j using 1
         · simp [← limit.w (liftToFinsetObj F) ⟨⟨⟨Finset.singleton_subset_iff.2 hj⟩⟩⟩]
           rfl
-        · aesop_cat }
+        · simp }
 
 variable (C) (α)
 
diff --git a/Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean b/Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
index d978a5c54dda2..e9e831e516ae5 100644
--- a/Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
+++ b/Mathlib/CategoryTheory/Limits/Constructions/ZeroObjects.lean
@@ -32,7 +32,7 @@ def binaryFanZeroLeft (X : C) : BinaryFan (0 : C) X :=
 
 /-- The limit cone for the product with a zero object is limiting. -/
 def binaryFanZeroLeftIsLimit (X : C) : IsLimit (binaryFanZeroLeft X) :=
-  BinaryFan.isLimitMk (fun s => BinaryFan.snd s) (by aesop_cat) (by aesop_cat)
+  BinaryFan.isLimitMk (fun s => BinaryFan.snd s) (by aesop_cat) (by simp)
     (fun s m _ h₂ => by simpa using h₂)
 
 instance hasBinaryProduct_zero_left (X : C) : HasBinaryProduct (0 : C) X :=
@@ -57,7 +57,7 @@ def binaryFanZeroRight (X : C) : BinaryFan X (0 : C) :=
 
 /-- The limit cone for the product with a zero object is limiting. -/
 def binaryFanZeroRightIsLimit (X : C) : IsLimit (binaryFanZeroRight X) :=
-  BinaryFan.isLimitMk (fun s => BinaryFan.fst s) (by aesop_cat) (by aesop_cat)
+  BinaryFan.isLimitMk (fun s => BinaryFan.fst s) (by simp) (by aesop_cat)
     (fun s m h₁ _ => by simpa using h₁)
 
 instance hasBinaryProduct_zero_right (X : C) : HasBinaryProduct X (0 : C) :=
@@ -82,7 +82,7 @@ def binaryCofanZeroLeft (X : C) : BinaryCofan (0 : C) X :=
 
 /-- The colimit cocone for the coproduct with a zero object is colimiting. -/
 def binaryCofanZeroLeftIsColimit (X : C) : IsColimit (binaryCofanZeroLeft X) :=
-  BinaryCofan.isColimitMk (fun s => BinaryCofan.inr s) (by aesop_cat) (by aesop_cat)
+  BinaryCofan.isColimitMk (fun s => BinaryCofan.inr s) (by aesop_cat) (by simp)
     (fun s m _ h₂ => by simpa using h₂)
 
 instance hasBinaryCoproduct_zero_left (X : C) : HasBinaryCoproduct (0 : C) X :=
@@ -107,7 +107,7 @@ def binaryCofanZeroRight (X : C) : BinaryCofan X (0 : C) :=
 
 /-- The colimit cocone for the coproduct with a zero object is colimiting. -/
 def binaryCofanZeroRightIsColimit (X : C) : IsColimit (binaryCofanZeroRight X) :=
-  BinaryCofan.isColimitMk (fun s => BinaryCofan.inl s) (by aesop_cat) (by aesop_cat)
+  BinaryCofan.isColimitMk (fun s => BinaryCofan.inl s) (by simp) (by aesop_cat)
     (fun s m h₁ _ => by simpa using h₁)
 
 instance hasBinaryCoproduct_zero_right (X : C) : HasBinaryCoproduct X (0 : C) :=
diff --git a/Mathlib/CategoryTheory/Limits/HasLimits.lean b/Mathlib/CategoryTheory/Limits/HasLimits.lean
index 27bcb80063f88..c3297674c5db3 100644
--- a/Mathlib/CategoryTheory/Limits/HasLimits.lean
+++ b/Mathlib/CategoryTheory/Limits/HasLimits.lean
@@ -225,13 +225,13 @@ def limit.isoLimitCone {F : J ⥤ C} [HasLimit F] (t : LimitCone F) : limit F 
 theorem limit.isoLimitCone_hom_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
     (limit.isoLimitCone t).hom ≫ t.cone.π.app j = limit.π F j := by
   dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
-  aesop_cat
+  simp
 
 @[reassoc (attr := simp)]
 theorem limit.isoLimitCone_inv_π {F : J ⥤ C} [HasLimit F] (t : LimitCone F) (j : J) :
     (limit.isoLimitCone t).inv ≫ limit.π F j = t.cone.π.app j := by
   dsimp [limit.isoLimitCone, IsLimit.conePointUniqueUpToIso]
-  aesop_cat
+  simp
 
 @[ext]
 theorem limit.hom_ext {F : J ⥤ C} [HasLimit F] {X : C} {f f' : X ⟶ limit F}
@@ -750,13 +750,13 @@ def colimit.isoColimitCocone {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F)
 theorem colimit.isoColimitCocone_ι_hom {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
     colimit.ι F j ≫ (colimit.isoColimitCocone t).hom = t.cocone.ι.app j := by
   dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
-  aesop_cat
+  simp
 
 @[reassoc (attr := simp)]
 theorem colimit.isoColimitCocone_ι_inv {F : J ⥤ C} [HasColimit F] (t : ColimitCocone F) (j : J) :
     t.cocone.ι.app j ≫ (colimit.isoColimitCocone t).inv = colimit.ι F j := by
   dsimp [colimit.isoColimitCocone, IsColimit.coconePointUniqueUpToIso]
-  aesop_cat
+  simp
 
 @[ext]
 theorem colimit.hom_ext {F : J ⥤ C} [HasColimit F] {X : C} {f f' : colimit F ⟶ X}
diff --git a/Mathlib/CategoryTheory/Limits/IsLimit.lean b/Mathlib/CategoryTheory/Limits/IsLimit.lean
index d0aebd2e0120a..6c1343fba3041 100644
--- a/Mathlib/CategoryTheory/Limits/IsLimit.lean
+++ b/Mathlib/CategoryTheory/Limits/IsLimit.lean
@@ -263,8 +263,8 @@ def conePointsIsoOfNatIso {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit
     (w : F ≅ G) : s.pt ≅ t.pt where
   hom := Q.map s w.hom
   inv := P.map t w.inv
-  hom_inv_id := P.hom_ext (by aesop_cat)
-  inv_hom_id := Q.hom_ext (by aesop_cat)
+  hom_inv_id := P.hom_ext (by simp)
+  inv_hom_id := Q.hom_ext (by simp)
 
 @[reassoc]
 theorem conePointsIsoOfNatIso_hom_comp {F G : J ⥤ C} {s : Cone F} {t : Cone G} (P : IsLimit s)
@@ -723,8 +723,8 @@ def coconePointsIsoOfNatIso {F G : J ⥤ C} {s : Cocone F} {t : Cocone G} (P : I
     (Q : IsColimit t) (w : F ≅ G) : s.pt ≅ t.pt where
   hom := P.map t w.hom
   inv := Q.map s w.inv
-  hom_inv_id := P.hom_ext (by aesop_cat)
-  inv_hom_id := Q.hom_ext (by aesop_cat)
+  hom_inv_id := P.hom_ext (by simp)
+  inv_hom_id := Q.hom_ext (by simp)
 
 @[reassoc]
 theorem comp_coconePointsIsoOfNatIso_hom {F G : J ⥤ C} {s : Cocone F} {t : Cocone G}
diff --git a/Mathlib/CategoryTheory/Limits/MonoCoprod.lean b/Mathlib/CategoryTheory/Limits/MonoCoprod.lean
index 9922662f9f26a..868732f7d96d1 100644
--- a/Mathlib/CategoryTheory/Limits/MonoCoprod.lean
+++ b/Mathlib/CategoryTheory/Limits/MonoCoprod.lean
@@ -60,7 +60,7 @@ theorem binaryCofan_inr {A B : C} [MonoCoprod C] (c : BinaryCofan A B) (hc : IsC
     Mono c.inr := by
   haveI hc' : IsColimit (BinaryCofan.mk c.inr c.inl) :=
     BinaryCofan.IsColimit.mk _ (fun f₁ f₂ => hc.desc (BinaryCofan.mk f₂ f₁))
-      (by aesop_cat) (by aesop_cat)
+      (by simp) (by simp)
       (fun f₁ f₂ m h₁ h₂ => BinaryCofan.IsColimit.hom_ext hc (by aesop_cat) (by aesop_cat))
   exact binaryCofan_inl _ hc'
 
diff --git a/Mathlib/CategoryTheory/Limits/Opposites.lean b/Mathlib/CategoryTheory/Limits/Opposites.lean
index 6c32f2d694aba..76a2af3431f75 100644
--- a/Mathlib/CategoryTheory/Limits/Opposites.lean
+++ b/Mathlib/CategoryTheory/Limits/Opposites.lean
@@ -888,7 +888,7 @@ theorem unop_fst {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocon
     c.unop.fst = c.inl.unop := by simp
 
 theorem unop_snd {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
-    c.unop.snd = c.inr.unop := by aesop_cat
+    c.unop.snd = c.inr.unop := by simp
 
 -- Porting note: it was originally @[simps (config := lemmasOnly)]
 /-- The obvious map `PushoutCocone f.op g.op → PullbackCone f g` -/
@@ -898,10 +898,10 @@ def op {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) : Pullbac
     (Cone.whisker walkingSpanOpEquiv.inverse (Cocone.op c))
 
 theorem op_fst {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
-    c.op.fst = c.inl.op := by aesop_cat
+    c.op.fst = c.inl.op := by simp
 
 theorem op_snd {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : PushoutCocone f g) :
-    c.op.snd = c.inr.op := by aesop_cat
+    c.op.snd = c.inr.op := by simp
 
 end PushoutCocone
 
@@ -917,10 +917,10 @@ def unop {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
       (Cone.whisker walkingSpanOpEquiv.functor c))
 
 theorem unop_inl {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
-    c.unop.inl = c.fst.unop := by aesop_cat
+    c.unop.inl = c.fst.unop := by simp
 
 theorem unop_inr {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
-    c.unop.inr = c.snd.unop := by aesop_cat
+    c.unop.inr = c.snd.unop := by simp
 
 /-- The obvious map `PullbackCone f g → PushoutCocone f.op g.op` -/
 @[simps!]
@@ -929,10 +929,10 @@ def op {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : PushoutC
     (Cocone.whisker walkingCospanOpEquiv.inverse (Cone.op c))
 
 theorem op_inl {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
-    c.op.inl = c.fst.op := by aesop_cat
+    c.op.inl = c.fst.op := by simp
 
 theorem op_inr {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) :
-    c.op.inr = c.snd.op := by aesop_cat
+    c.op.inr = c.snd.op := by simp
 
 /-- If `c` is a pullback cone, then `c.op.unop` is isomorphic to `c`. -/
 def opUnop {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z} (c : PullbackCone f g) : c.op.unop ≅ c :=
diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
index 550f8c8bea18d..95581e7fd2454 100644
--- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Biproducts.lean
@@ -237,7 +237,7 @@ theorem biproductComparison'_comp_biproductComparison :
 @[simps]
 def splitEpiBiproductComparison : SplitEpi (biproductComparison F f) where
   section_ := biproductComparison' F f
-  id := by aesop
+  id := by simp
 
 instance : IsSplitEpi (biproductComparison F f) :=
   IsSplitEpi.mk' (splitEpiBiproductComparison F f)
@@ -246,7 +246,7 @@ instance : IsSplitEpi (biproductComparison F f) :=
 @[simps]
 def splitMonoBiproductComparison' : SplitMono (biproductComparison' F f) where
   retraction := biproductComparison F f
-  id := by aesop
+  id := by simp
 
 instance : IsSplitMono (biproductComparison' F f) :=
   IsSplitMono.mk' (splitMonoBiproductComparison' F f)
@@ -321,7 +321,7 @@ theorem biprodComparison'_comp_biprodComparison :
 @[simps]
 def splitEpiBiprodComparison : SplitEpi (biprodComparison F X Y) where
   section_ := biprodComparison' F X Y
-  id := by aesop
+  id := by simp
 
 instance : IsSplitEpi (biprodComparison F X Y) :=
   IsSplitEpi.mk' (splitEpiBiprodComparison F X Y)
@@ -330,7 +330,7 @@ instance : IsSplitEpi (biprodComparison F X Y) :=
 @[simps]
 def splitMonoBiprodComparison' : SplitMono (biprodComparison' F X Y) where
   retraction := biprodComparison F X Y
-  id := by aesop
+  id := by simp
 
 instance : IsSplitMono (biprodComparison' F X Y) :=
   IsSplitMono.mk' (splitMonoBiprodComparison' F X Y)
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
index cf91656226688..28ea0694e2027 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
@@ -280,7 +280,7 @@ def whiskerToCone {f : J → C} (c : Bicone f) (g : K ≃ J) :
     (c.whisker g).toCone ≅
       (Cones.postcompose (Discrete.functorComp f g).inv).obj
         (c.toCone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
-  Cones.ext (Iso.refl _) (by aesop_cat)
+  Cones.ext (Iso.refl _) (by simp)
 
 /-- Taking the cocone of a whiskered bicone results in a cone isomorphic to one gained
 by whiskering the cocone and precomposing with a suitable isomorphism. -/
@@ -288,7 +288,7 @@ def whiskerToCocone {f : J → C} (c : Bicone f) (g : K ≃ J) :
     (c.whisker g).toCocone ≅
       (Cocones.precompose (Discrete.functorComp f g).hom).obj
         (c.toCocone.whisker (Discrete.functor (Discrete.mk ∘ g))) :=
-  Cocones.ext (Iso.refl _) (by aesop_cat)
+  Cocones.ext (Iso.refl _) (by simp)
 
 /-- Whiskering a bicone with an equivalence between types preserves being a bilimit bicone. -/
 noncomputable def whiskerIsBilimitIff {f : J → C} (c : Bicone f) (g : K ≃ J) :
@@ -625,7 +625,7 @@ instance biproduct.map_epi {f g : J → C} [HasBiproduct f] [HasBiproduct g] (p
       ι_colimMap_assoc, Discrete.functor_obj_eq_as, Discrete.natTrans_app, colimit.ι_desc_assoc,
       Cofan.mk_pt, Cofan.mk_ι_app, ι_π, ι_π_assoc]
     split
-    all_goals aesop
+    all_goals simp_all
   rw [this]
   infer_instance
 
@@ -1757,7 +1757,7 @@ instance biprod.map_epi {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
 instance prod.map_epi {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Epi f]
     [Epi g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Epi (prod.map f g) := by
   rw [show prod.map f g = (biprod.isoProd _ _).inv ≫ biprod.map f g ≫
-    (biprod.isoProd _ _).hom by aesop]
+    (biprod.isoProd _ _).hom by simp]
   infer_instance
 
 instance biprod.map_mono {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
@@ -1769,7 +1769,7 @@ instance biprod.map_mono {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
 instance coprod.map_mono {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) [Mono f]
     [Mono g] [HasBinaryBiproduct W X] [HasBinaryBiproduct Y Z] : Mono (coprod.map f g) := by
   rw [show coprod.map f g = (biprod.isoCoprod _ _).inv ≫ biprod.map f g ≫
-    (biprod.isoCoprod _ _).hom by aesop]
+    (biprod.isoCoprod _ _).hom by simp]
   infer_instance
 
 section BiprodKernel
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
index 36a0a6e065433..fdf4259edc924 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Equalizers.lean
@@ -533,7 +533,7 @@ theorem Cofork.IsColimit.homIso_natural {X Y : C} {f g : X ⟶ Y} {t : Cofork f
 def Cone.ofFork {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) : Cone F where
   pt := t.pt
   π :=
-    { app := fun X => t.π.app X ≫ eqToHom (by aesop)
+    { app := fun X => t.π.app X ≫ eqToHom (by simp)
       naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp [t.condition]}}
 
 /-- This is a helper construction that can be useful when verifying that a category has all
@@ -548,23 +548,23 @@ def Cocone.ofCofork {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.
     Cocone F where
   pt := t.pt
   ι :=
-    { app := fun X => eqToHom (by aesop) ≫ t.ι.app X
+    { app := fun X => eqToHom (by simp) ≫ t.ι.app X
       naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp [t.condition]}}
 
 @[simp]
 theorem Cone.ofFork_π {F : WalkingParallelPair ⥤ C} (t : Fork (F.map left) (F.map right)) (j) :
-    (Cone.ofFork t).π.app j = t.π.app j ≫ eqToHom (by aesop) := rfl
+    (Cone.ofFork t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl
 
 @[simp]
 theorem Cocone.ofCofork_ι {F : WalkingParallelPair ⥤ C} (t : Cofork (F.map left) (F.map right))
-    (j) : (Cocone.ofCofork t).ι.app j = eqToHom (by aesop) ≫ t.ι.app j := rfl
+    (j) : (Cocone.ofCofork t).ι.app j = eqToHom (by simp) ≫ t.ι.app j := rfl
 
 /-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
     `parallelPair (F.map left) (F.map right)` and a cone on `F`, we get a fork on
     `F.map left` and `F.map right`. -/
 def Fork.ofCone {F : WalkingParallelPair ⥤ C} (t : Cone F) : Fork (F.map left) (F.map right) where
   pt := t.pt
-  π := { app := fun X => t.π.app X ≫ eqToHom (by aesop)
+  π := { app := fun X => t.π.app X ≫ eqToHom (by simp)
          naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp}}
 
 /-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
@@ -573,16 +573,16 @@ def Fork.ofCone {F : WalkingParallelPair ⥤ C} (t : Cone F) : Fork (F.map left)
 def Cofork.ofCocone {F : WalkingParallelPair ⥤ C} (t : Cocone F) :
     Cofork (F.map left) (F.map right) where
   pt := t.pt
-  ι := { app := fun X => eqToHom (by aesop) ≫ t.ι.app X
+  ι := { app := fun X => eqToHom (by simp) ≫ t.ι.app X
          naturality := by rintro _ _ (_|_|_) <;> {dsimp; simp}}
 
 @[simp]
 theorem Fork.ofCone_π {F : WalkingParallelPair ⥤ C} (t : Cone F) (j) :
-    (Fork.ofCone t).π.app j = t.π.app j ≫ eqToHom (by aesop) := rfl
+    (Fork.ofCone t).π.app j = t.π.app j ≫ eqToHom (by simp) := rfl
 
 @[simp]
 theorem Cofork.ofCocone_ι {F : WalkingParallelPair ⥤ C} (t : Cocone F) (j) :
-    (Cofork.ofCocone t).ι.app j = eqToHom (by aesop) ≫ t.ι.app j := rfl
+    (Cofork.ofCocone t).ι.app j = eqToHom (by simp) ≫ t.ι.app j := rfl
 
 @[simp]
 theorem Fork.ι_postcompose {f' g' : X ⟶ Y} {α : parallelPair f g ⟶ parallelPair f' g'}
@@ -710,7 +710,7 @@ theorem equalizer.condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g :=
 /-- The equalizer built from `equalizer.ι f g` is limiting. -/
 noncomputable def equalizerIsEqualizer : IsLimit (Fork.ofι (equalizer.ι f g)
     (equalizer.condition f g)) :=
-  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by aesop))
+  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by simp))
 
 variable {f g}
 
@@ -859,7 +859,7 @@ theorem coequalizer.condition : f ≫ coequalizer.π f g = g ≫ coequalizer.π
 /-- The cofork built from `coequalizer.π f g` is colimiting. -/
 noncomputable def coequalizerIsCoequalizer :
     IsColimit (Cofork.ofπ (coequalizer.π f g) (coequalizer.condition f g)) :=
-  IsColimit.ofIsoColimit (colimit.isColimit _) (Cofork.ext (Iso.refl _) (by aesop))
+  IsColimit.ofIsoColimit (colimit.isColimit _) (Cofork.ext (Iso.refl _) (by simp))
 
 variable {f g}
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
index fec3f30cad1ff..f11792f5eaace 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Images.lean
@@ -613,7 +613,7 @@ attribute [inherit_doc ImageMap] ImageMap.map ImageMap.map_ι
 attribute [-simp, nolint simpNF] ImageMap.mk.injEq
 
 instance inhabitedImageMap {f : Arrow C} [HasImage f.hom] : Inhabited (ImageMap (𝟙 f)) :=
-  ⟨⟨𝟙 _, by aesop⟩⟩
+  ⟨⟨𝟙 _, by simp⟩⟩
 
 attribute [reassoc (attr := simp)] ImageMap.map_ι
 
@@ -717,8 +717,8 @@ theorem image.factor_map :
 theorem image.map_ι : image.map sq ≫ image.ι g.hom = image.ι f.hom ≫ sq.right := by simp
 
 theorem image.map_homMk'_ι {X Y P Q : C} {k : X ⟶ Y} [HasImage k] {l : P ⟶ Q} [HasImage l]
-    {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n) [HasImageMap (Arrow.homMk' w)] :
-    image.map (Arrow.homMk' w) ≫ image.ι l = image.ι k ≫ n :=
+    {m : X ⟶ P} {n : Y ⟶ Q} (w : m ≫ l = k ≫ n) [HasImageMap (Arrow.homMk' _ _ w)] :
+    image.map (Arrow.homMk' _ _ w) ≫ image.ι l = image.ι k ≫ n :=
   image.map_ι _
 
 section
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
index de6ee324b9d3d..a33d65333e024 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/IsTerminal.lean
@@ -57,11 +57,11 @@ abbrev IsInitial (X : C) :=
 
 /-- An object `Y` is terminal iff for every `X` there is a unique morphism `X ⟶ Y`. -/
 def isTerminalEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (Y : C) :
-    IsLimit (⟨Y, by aesop_cat, by aesop_cat⟩ : Cone F) ≃ ∀ X : C, Unique (X ⟶ Y) where
+    IsLimit (⟨Y, by aesop_cat, by simp⟩ : Cone F) ≃ ∀ X : C, Unique (X ⟶ Y) where
   toFun t X :=
-    { default := t.lift ⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩
+    { default := t.lift ⟨X, ⟨by aesop_cat, by simp⟩⟩
       uniq := fun f =>
-        t.uniq ⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩ f (by aesop_cat) }
+        t.uniq ⟨X, ⟨by aesop_cat, by simp⟩⟩ f (by simp) }
   invFun u :=
     { lift := fun s => (u s.pt).default
       uniq := fun s _ _ => (u s.pt).2 _ }
@@ -103,10 +103,10 @@ def IsTerminal.equivOfIso {X Y : C} (e : X ≅ Y) :
 
 /-- An object `X` is initial iff for every `Y` there is a unique morphism `X ⟶ Y`. -/
 def isInitialEquivUnique (F : Discrete.{0} PEmpty.{1} ⥤ C) (X : C) :
-    IsColimit (⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y) where
+    IsColimit (⟨X, ⟨by aesop_cat, by simp⟩⟩ : Cocone F) ≃ ∀ Y : C, Unique (X ⟶ Y) where
   toFun t X :=
-    { default := t.desc ⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩
-      uniq := fun f => t.uniq ⟨X, ⟨by aesop_cat, by aesop_cat⟩⟩ f (by aesop_cat) }
+    { default := t.desc ⟨X, ⟨by aesop_cat, by simp⟩⟩
+      uniq := fun f => t.uniq ⟨X, ⟨by aesop_cat, by simp⟩⟩ f (by simp) }
   invFun u :=
     { desc := fun s => (u s.pt).default
       uniq := fun s _ _ => (u s.pt).2 _ }
@@ -152,7 +152,7 @@ def IsTerminal.from {X : C} (t : IsTerminal X) (Y : C) : Y ⟶ X :=
 
 /-- Any two morphisms to a terminal object are equal. -/
 theorem IsTerminal.hom_ext {X Y : C} (t : IsTerminal X) (f g : Y ⟶ X) : f = g :=
-  IsLimit.hom_ext t (by aesop_cat)
+  IsLimit.hom_ext t (by simp)
 
 @[simp]
 theorem IsTerminal.comp_from {Z : C} (t : IsTerminal Z) {X Y : C} (f : X ⟶ Y) :
@@ -169,7 +169,7 @@ def IsInitial.to {X : C} (t : IsInitial X) (Y : C) : X ⟶ Y :=
 
 /-- Any two morphisms from an initial object are equal. -/
 theorem IsInitial.hom_ext {X Y : C} (t : IsInitial X) (f g : X ⟶ Y) : f = g :=
-  IsColimit.hom_ext t (by aesop_cat)
+  IsColimit.hom_ext t (by simp)
 
 @[simp]
 theorem IsInitial.to_comp {X : C} (t : IsInitial X) {Y Z : C} (f : Y ⟶ Z) : t.to Y ≫ f = t.to Z :=
@@ -217,12 +217,12 @@ variable (X : C) {F₁ : Discrete.{w} PEmpty ⥤ C} {F₂ : Discrete.{w'} PEmpty
     as long as the cone points are isomorphic. -/
 def isLimitChangeEmptyCone {c₁ : Cone F₁} (hl : IsLimit c₁) (c₂ : Cone F₂) (hi : c₁.pt ≅ c₂.pt) :
     IsLimit c₂ where
-  lift c := hl.lift ⟨c.pt, by aesop_cat, by aesop_cat⟩ ≫ hi.hom
+  lift c := hl.lift ⟨c.pt, by aesop_cat, by simp⟩ ≫ hi.hom
   uniq c f _ := by
     dsimp
     rw [← hl.uniq _ (f ≫ hi.inv) _]
     · simp only [Category.assoc, Iso.inv_hom_id, Category.comp_id]
-    · aesop_cat
+    · simp
 
 /-- Replacing an empty cone in `IsLimit` by another with the same cone point
     is an equivalence. -/
@@ -239,12 +239,12 @@ def isLimitEmptyConeEquiv (c₁ : Cone F₁) (c₂ : Cone F₂) (h : c₁.pt ≅
     as long as the cocone points are isomorphic. -/
 def isColimitChangeEmptyCocone {c₁ : Cocone F₁} (hl : IsColimit c₁) (c₂ : Cocone F₂)
     (hi : c₁.pt ≅ c₂.pt) : IsColimit c₂ where
-  desc c := hi.inv ≫ hl.desc ⟨c.pt, by aesop_cat, by aesop_cat⟩
+  desc c := hi.inv ≫ hl.desc ⟨c.pt, by aesop_cat, by simp⟩
   uniq c f _ := by
     dsimp
     rw [← hl.uniq _ (hi.hom ≫ f) _]
     · simp only [Iso.inv_hom_id_assoc]
-    · aesop_cat
+    · simp
 
 /-- Replacing an empty cocone in `IsColimit` by another with the same cocone point
     is an equivalence. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
index 202f266d2d66f..6e11689c3fc8b 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
@@ -275,7 +275,7 @@ theorem kernel.condition : kernel.ι f ≫ f = 0 :=
 
 /-- The kernel built from `kernel.ι f` is limiting. -/
 def kernelIsKernel : IsLimit (Fork.ofι (kernel.ι f) ((kernel.condition f).trans comp_zero.symm)) :=
-  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by aesop_cat))
+  IsLimit.ofIsoLimit (limit.isLimit _) (Fork.ext (Iso.refl _) (by simp))
 
 /-- Given any morphism `k : W ⟶ X` satisfying `k ≫ f = 0`, `k` factors through `kernel.ι f`
     via `kernel.lift : W ⟶ kernel f`. -/
@@ -425,8 +425,8 @@ instance hasKernel_iso_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [IsIso f] [H
     HasKernel (f ≫ g) where
   exists_limit :=
     ⟨{  cone := KernelFork.ofι (kernel.ι g ≫ inv f) (by simp)
-        isLimit := isLimitAux _ (fun s => kernel.lift _ (s.ι ≫ f) (by aesop_cat))
-            (by aesop_cat) fun s m w => by
+        isLimit := isLimitAux _ (fun s => kernel.lift _ (s.ι ≫ f) (by simp))
+            (by simp) fun s m w => by
           simp_rw [← w]
           symm
           apply equalizer.hom_ext
@@ -751,7 +751,7 @@ lemma colimit_ι_zero_cokernel_desc {C : Type*} [Category C]
     [HasZeroMorphisms C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (h : f ≫ g = 0) [HasCokernel f] :
     colimit.ι (parallelPair f 0) WalkingParallelPair.zero ≫ cokernel.desc f g h = 0 := by
   rw [(colimit.w (parallelPair f 0) WalkingParallelPairHom.left).symm]
-  aesop_cat
+  simp
 
 @[simp]
 theorem cokernel.desc_zero {W : C} {h} : cokernel.desc f (0 : Y ⟶ W) h = 0 := by
@@ -884,7 +884,7 @@ instance hasCokernel_comp_iso {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) [HasCokern
           isColimitAux _
             (fun s =>
               cokernel.desc _ (g ≫ s.π) (by rw [← Category.assoc, CokernelCofork.condition]))
-            (by aesop_cat) fun s m w => by
+            (by simp) fun s m w => by
             simp_rw [← w]
             symm
             apply coequalizer.hom_ext
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
index 02cc099007693..9cd40dec3a39b 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@@ -565,7 +565,7 @@ instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
   exists_limit := Nonempty.intro
     { cone := Fan.mk (∏ᶜ fun i => ∏ᶜ g i) (fun X => Pi.π (fun i => ∏ᶜ g i) X.1 ≫ Pi.π (g X.1) X.2)
       isLimit := mkFanLimit _ (fun s => Pi.lift fun b => Pi.lift fun c => s.proj ⟨b, c⟩)
-        (by aesop_cat)
+        (by simp)
         (by intro s m w; simp only [Fan.mk_pt]; symm; ext i x; simp_all [Sigma.forall]) }
 
 /-- An iterated product is a product over a sigma type. -/
@@ -586,7 +586,7 @@ instance {ι : Type*} (f : ι → Type*) (g : (i : ι) → (f i) → C)
         (fun X => Sigma.ι (g X.1) X.2 ≫ Sigma.ι (fun i => ∐ g i) X.1)
       isColimit := mkCofanColimit _
         (fun s => Sigma.desc fun b => Sigma.desc fun c => s.inj ⟨b, c⟩)
-        (by aesop_cat)
+        (by simp)
         (by intro s m w; simp only [Cofan.mk_pt]; symm; ext i x; simp_all [Sigma.forall]) }
 
 /-- An iterated coproduct is a coproduct over a sigma type. -/
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
index 14f78f89b5b08..bc2c51f174f0e 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
@@ -89,27 +89,27 @@ theorem cocone_inr (s : CommSq f g h i) : s.cocone.inr = i :=
 a commutative square identifies to the cocone of the flipped commutative square in
 the opposite category -/
 def coneOp (p : CommSq f g h i) : p.cone.op ≅ p.flip.op.cocone :=
-  PushoutCocone.ext (Iso.refl _) (by aesop_cat) (by aesop_cat)
+  PushoutCocone.ext (Iso.refl _) (by simp) (by simp)
 
 /-- The pullback cone in the opposite category associated to the cocone of
 a commutative square identifies to the cone of the flipped commutative square in
 the opposite category -/
 def coconeOp (p : CommSq f g h i) : p.cocone.op ≅ p.flip.op.cone :=
-  PullbackCone.ext (Iso.refl _) (by aesop_cat) (by aesop_cat)
+  PullbackCone.ext (Iso.refl _) (by simp) (by simp)
 
 /-- The pushout cocone obtained from the pullback cone associated to a
 commutative square in the opposite category identifies to the cocone associated
 to the flipped square. -/
 def coneUnop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z} (p : CommSq f g h i) :
     p.cone.unop ≅ p.flip.unop.cocone :=
-  PushoutCocone.ext (Iso.refl _) (by aesop_cat) (by aesop_cat)
+  PushoutCocone.ext (Iso.refl _) (by simp) (by simp)
 
 /-- The pullback cone obtained from the pushout cone associated to a
 commutative square in the opposite category identifies to the cone associated
 to the flipped square. -/
 def coconeUnop {W X Y Z : Cᵒᵖ} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z} {i : Y ⟶ Z}
     (p : CommSq f g h i) : p.cocone.unop ≅ p.flip.unop.cone :=
-  PullbackCone.ext (Iso.refl _) (by aesop_cat) (by aesop_cat)
+  PullbackCone.ext (Iso.refl _) (by simp) (by simp)
 
 end CommSq
 
@@ -221,7 +221,7 @@ lemma hom_ext (hP : IsPullback fst snd f g) {W : C} {k l : W ⟶ P}
 theorem of_isLimit {c : PullbackCone f g} (h : Limits.IsLimit c) : IsPullback c.fst c.snd f g :=
   { w := c.condition
     isLimit' := ⟨IsLimit.ofIsoLimit h (Limits.PullbackCone.ext (Iso.refl _)
-      (by aesop_cat) (by aesop_cat))⟩ }
+      (by simp) (by simp))⟩ }
 
 /-- A variant of `of_isLimit` that is more useful with `apply`. -/
 theorem of_isLimit' (w : CommSq fst snd f g) (h : Limits.IsLimit w.cone) :
@@ -345,7 +345,7 @@ theorem of_horiz_isIso [IsIso fst] [IsIso g] (sq : CommSq fst snd f g) : IsPullb
   of_isLimit' sq
     (by
       refine
-        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by aesop_cat)
+        PullbackCone.IsLimit.mk _ (fun s => s.fst ≫ inv fst) (by simp)
           (fun s => ?_) (by aesop_cat)
       simp only [← cancel_mono g, Category.assoc, ← sq.w, IsIso.inv_hom_id_assoc, s.condition])
 
@@ -431,7 +431,7 @@ theorem of_isColimit {c : PushoutCocone f g} (h : Limits.IsColimit c) : IsPushou
   { w := c.condition
     isColimit' :=
       ⟨IsColimit.ofIsoColimit h (Limits.PushoutCocone.ext (Iso.refl _)
-        (by aesop_cat) (by aesop_cat))⟩ }
+        (by simp) (by simp))⟩ }
 
 /-- A variant of `of_isColimit` that is more useful with `apply`. -/
 theorem of_isColimit' (w : CommSq f g inl inr) (h : Limits.IsColimit w.cocone) :
@@ -1161,7 +1161,7 @@ theorem of_horiz_isIso [IsIso f] [IsIso inr] (sq : CommSq f g inl inr) : IsPusho
     (by
       refine
         PushoutCocone.IsColimit.mk _ (fun s => inv inr ≫ s.inr) (fun s => ?_)
-          (by aesop_cat) (by aesop_cat)
+          (by simp) (by simp)
       simp only [← cancel_epi f, s.condition, sq.w_assoc, IsIso.hom_inv_id_assoc])
 
 theorem of_vert_isIso [IsIso g] [IsIso inl] (sq : CommSq f g inl inr) : IsPushout f g inl inr :=
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
index 01bb011074096..ddd0fc6d43918 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Pullback/Square.lean
@@ -79,7 +79,7 @@ lemma IsPullback.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPullback)
   refine CategoryTheory.IsPullback.of_iso h
     (evaluation₁.mapIso e) (evaluation₂.mapIso e)
     (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-  all_goals aesop_cat
+  all_goals simp
 
 lemma IsPullback.iff_of_iso {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
     sq₁.IsPullback ↔ sq₂.IsPullback :=
@@ -90,7 +90,7 @@ lemma IsPushout.of_iso {sq₁ sq₂ : Square C} (h : sq₁.IsPushout)
   refine CategoryTheory.IsPushout.of_iso h
     (evaluation₁.mapIso e) (evaluation₂.mapIso e)
     (evaluation₃.mapIso e) (evaluation₄.mapIso e) ?_ ?_ ?_ ?_
-  all_goals aesop_cat
+  all_goals simp
 
 lemma IsPushout.iff_of_iso {sq₁ sq₂ : Square C} (e : sq₁ ≅ sq₂) :
     sq₁.IsPushout ↔ sq₂.IsPushout :=
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean b/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
index abcc9d116cda0..d1c5d29b44ebf 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Reflexive.lean
@@ -543,7 +543,7 @@ lemma reflexiveCoforkEquivCofork_functor_obj_π (G : ReflexiveCofork F) :
     ((reflexiveCoforkEquivCofork F).functor.obj G).π = G.π := by
   dsimp [reflexiveCoforkEquivCofork]
   rw [ReflexiveCofork.π, Cofork.π]
-  aesop_cat
+  simp
 
 @[simp]
 lemma reflexiveCoforkEquivCofork_inverse_obj_π
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
index 2abdbdfda2ec4..e5f5d8bc1363b 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/StrongEpi.lean
@@ -164,11 +164,11 @@ end
 
 /-- A strong epimorphism that is a monomorphism is an isomorphism. -/
 theorem isIso_of_mono_of_strongEpi (f : P ⟶ Q) [Mono f] [StrongEpi f] : IsIso f :=
-  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
+  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩
 
 /-- A strong monomorphism that is an epimorphism is an isomorphism. -/
 theorem isIso_of_epi_of_strongMono (f : P ⟶ Q) [Epi f] [StrongMono f] : IsIso f :=
-  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by aesop_cat⟩⟩
+  ⟨⟨(CommSq.mk (show 𝟙 P ≫ f = f ≫ 𝟙 Q by simp)).lift, by simp⟩⟩
 
 section
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
index d24c05e73cd2c..e3f907ea79b4a 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Terminal.lean
@@ -43,7 +43,7 @@ section Univ
 variable (X : C) {F₁ : Discrete.{w} PEmpty ⥤ C} {F₂ : Discrete.{w'} PEmpty ⥤ C}
 
 theorem hasTerminalChangeDiagram (h : HasLimit F₁) : HasLimit F₂ :=
-  ⟨⟨⟨⟨limit F₁, by aesop_cat, by aesop_cat⟩,
+  ⟨⟨⟨⟨limit F₁, by aesop_cat, by simp⟩,
     isLimitChangeEmptyCone C (limit.isLimit F₁) _ (eqToIso rfl)⟩⟩⟩
 
 theorem hasTerminalChangeUniverse [h : HasLimitsOfShape (Discrete.{w} PEmpty) C] :
@@ -51,7 +51,7 @@ theorem hasTerminalChangeUniverse [h : HasLimitsOfShape (Discrete.{w} PEmpty) C]
   has_limit _ := hasTerminalChangeDiagram C (h.1 (Functor.empty C))
 
 theorem hasInitialChangeDiagram (h : HasColimit F₁) : HasColimit F₂ :=
-  ⟨⟨⟨⟨colimit F₁, by aesop_cat, by aesop_cat⟩,
+  ⟨⟨⟨⟨colimit F₁, by aesop_cat, by simp⟩,
     isColimitChangeEmptyCocone C (colimit.isColimit F₁) _ (eqToIso rfl)⟩⟩⟩
 
 theorem hasInitialChangeUniverse [h : HasColimitsOfShape (Discrete.{w} PEmpty) C] :
@@ -92,7 +92,7 @@ theorem hasTerminal_of_unique (X : C) [∀ Y, Nonempty (Y ⟶ X)] [∀ Y, Subsin
     ⟨Classical.inhabited_of_nonempty', (Subsingleton.elim · _)⟩⟩
 
 theorem IsTerminal.hasTerminal {X : C} (h : IsTerminal X) : HasTerminal C :=
-  { has_limit := fun F => HasLimit.mk ⟨⟨X, by aesop_cat, by aesop_cat⟩,
+  { has_limit := fun F => HasLimit.mk ⟨⟨X, by aesop_cat, by simp⟩,
     isLimitChangeEmptyCone _ h _ (Iso.refl _)⟩ }
 
 /-- We can more explicitly show that a category has an initial object by specifying the object,
@@ -104,7 +104,7 @@ theorem hasInitial_of_unique (X : C) [∀ Y, Nonempty (X ⟶ Y)] [∀ Y, Subsing
 
 theorem IsInitial.hasInitial {X : C} (h : IsInitial X) : HasInitial C where
   has_colimit F :=
-    HasColimit.mk ⟨⟨X, by aesop_cat, by aesop_cat⟩, isColimitChangeEmptyCocone _ h _ (Iso.refl _)⟩
+    HasColimit.mk ⟨⟨X, by aesop_cat, by simp⟩, isColimitChangeEmptyCocone _ h _ (Iso.refl _)⟩
 
 /-- The map from an object to the terminal object. -/
 abbrev terminal.from [HasTerminal C] (P : C) : P ⟶ ⊤_ C :=
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/Types.lean b/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
index f6dfbe28fd6cb..df7ea12153d1c 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/Types.lean
@@ -924,7 +924,7 @@ lemma pushoutCocone_inl_eq_inr_iff_of_isColimit {c : PushoutCocone f g} (hc : Is
     c.inl x₁ = c.inr x₂ ↔ ∃ (s : S), f s = x₁ ∧ g s = x₂ := by
   rw [pushoutCocone_inl_eq_inr_iff_of_iso
     (Cocones.ext (IsColimit.coconePointUniqueUpToIso hc (Pushout.isColimitCocone f g))
-    (by aesop_cat))]
+    (by simp))]
   have := (mono_iff_injective f).2 h₁
   apply Pushout.inl_eq_inr_iff
 
diff --git a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
index 4670206841758..06d17c50c7d91 100644
--- a/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
+++ b/Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean
@@ -330,9 +330,9 @@ theorem eq_lift_of_comp_eq (g : X ⟶ widePullback _ _ arrows) :
   · apply h1
 
 theorem hom_eq_lift (g : X ⟶ widePullback _ _ arrows) :
-    g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (by aesop_cat) := by
+    g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (by simp) := by
   apply eq_lift_of_comp_eq
-  · aesop_cat
+  · simp
   · rfl  -- Porting note: quite a few missing refl's in aesop_cat now
 
 @[ext 1100]
@@ -400,7 +400,7 @@ theorem hom_eq_desc (g : widePushout _ _ arrows ⟶ X) :
         rw [← Category.assoc]
         simp := by
   apply eq_desc_of_comp_eq
-  · aesop_cat
+  · simp
   · rfl -- Porting note: another missing rfl
 
 @[ext 1100]
diff --git a/Mathlib/CategoryTheory/Localization/Bifunctor.lean b/Mathlib/CategoryTheory/Localization/Bifunctor.lean
index e4556b6e608d8..7755ae9cca22e 100644
--- a/Mathlib/CategoryTheory/Localization/Bifunctor.lean
+++ b/Mathlib/CategoryTheory/Localization/Bifunctor.lean
@@ -168,8 +168,8 @@ and `Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'` hold. -/
 noncomputable def lift₂NatIso (e : F₁ ≅ F₂) : F₁' ≅ F₂' where
   hom := lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' e.hom
   inv := lift₂NatTrans L₁ L₂ W₁ W₂ F₂ F₁ F₂' F₁' e.inv
-  hom_inv_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat)
-  inv_hom_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by aesop_cat)
+  hom_inv_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by simp)
+  inv_hom_id := natTrans₂_ext L₁ L₂ W₁ W₂ (by simp)
 
 end
 
diff --git a/Mathlib/CategoryTheory/Localization/Construction.lean b/Mathlib/CategoryTheory/Localization/Construction.lean
index b82770a4d5037..5bcd82a33e3e7 100644
--- a/Mathlib/CategoryTheory/Localization/Construction.lean
+++ b/Mathlib/CategoryTheory/Localization/Construction.lean
@@ -154,7 +154,7 @@ def lift : W.Localization ⥤ D :=
       -- Porting note: rest of proof was `rcases r with ⟨⟩; tidy`
       rcases r with (_|_|⟨f,hf⟩|⟨f,hf⟩)
       · aesop_cat
-      · aesop_cat
+      · simp
       all_goals
         dsimp
         haveI := hG f hf
diff --git a/Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean b/Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
index 2adefbca8f183..b7da168c46084 100644
--- a/Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
+++ b/Mathlib/CategoryTheory/Localization/DerivabilityStructure/Constructor.lean
@@ -90,7 +90,7 @@ lemma isConnected :
       (isPreconnected_zigzag (RightResolution.mk (𝟙 _) (W₂.id_mem _))
         (RightResolution.mk ρ.w.right ρ.hw.2))
   refine Zigzag.trans ?_ (Zigzag.trans this ?_)
-  · exact Zigzag.of_hom (eqToHom (by aesop))
+  · exact Zigzag.of_hom (eqToHom (by simp))
   · apply Zigzag.of_inv
     refine CostructuredArrow.homMk (StructuredArrow.homMk ρ.X₁.hom (by simp)) ?_
     ext
diff --git a/Mathlib/CategoryTheory/Localization/Predicate.lean b/Mathlib/CategoryTheory/Localization/Predicate.lean
index bc2855fa278ac..4178f7ade448c 100644
--- a/Mathlib/CategoryTheory/Localization/Predicate.lean
+++ b/Mathlib/CategoryTheory/Localization/Predicate.lean
@@ -432,7 +432,9 @@ same `MorphismProperty C`, this is an equivalence of categories `D₁ ≌ D₂`.
 def uniq : D₁ ≌ D₂ :=
   (equivalenceFromModel L₁ W').symm.trans (equivalenceFromModel L₂ W')
 
-lemma uniq_symm : (uniq L₁ L₂ W').symm = uniq L₂ L₁ W' := rfl
+lemma uniq_symm : (uniq L₁ L₂ W').symm = uniq L₂ L₁ W' := by
+  dsimp [uniq, Equivalence.trans]
+  ext <;> aesop
 
 /-- The functor of equivalence of localized categories given by `Localization.uniq` is
 compatible with the localization functors. -/
diff --git a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
index b2025fc3fd6e4..2b1164339e414 100644
--- a/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
@@ -236,7 +236,7 @@ noncomputable def braidedCategoryOfFullyFaithful {C D : Type*} [Category C] [Cat
   braidedCategoryOfFaithful F
     (fun X Y => F.preimageIso
       ((μIso F _ _).symm ≪≫ β_ (F.obj X) (F.obj Y) ≪≫ (μIso F _ _)))
-    (by aesop_cat)
+    (by simp)
 
 section
 
diff --git a/Mathlib/CategoryTheory/Monoidal/End.lean b/Mathlib/CategoryTheory/Monoidal/End.lean
index ab0ce6bcf4ec1..2994d7b5dc0ef 100644
--- a/Mathlib/CategoryTheory/Monoidal/End.lean
+++ b/Mathlib/CategoryTheory/Monoidal/End.lean
@@ -141,7 +141,7 @@ theorem ε_naturality {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] :
 @[reassoc (attr := simp)]
 theorem η_naturality {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal]:
     (η F).app X ≫ (𝟙_ (C ⥤ C)).map f = (η F).app X ≫ f := by
-  aesop_cat
+  simp
 
 @[reassoc (attr := simp)]
 theorem μ_naturality {m n : M} {X Y : C} (f : X ⟶ Y) [F.LaxMonoidal] :
diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
index 84cdce3c91ae3..5125b23e93c80 100644
--- a/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Internal/Limits.lean
@@ -52,7 +52,7 @@ def limitCone (F : J ⥤ Mon_ C) : Cone F where
 -/
 def forgetMapConeLimitConeIso (F : J ⥤ Mon_ C) :
     (forget C).mapCone (limitCone F) ≅ limit.cone (F ⋙ forget C) :=
-  Cones.ext (Iso.refl _) (by aesop_cat)
+  Cones.ext (Iso.refl _) (by simp)
 
 /-- Implementation of `Mon_.hasLimitsOfShape`:
 the proposed cone over a functor `F : J ⥤ Mon_ C` is a limit cone.
diff --git a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
index 52293104297ba..407983573fdc0 100644
--- a/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
+++ b/Mathlib/CategoryTheory/Monoidal/Subcategory.lean
@@ -128,7 +128,7 @@ instance fullBraidedSubcategory : BraidedCategory (FullSubcategory P) :=
   braidedCategoryOfFaithful (fullSubcategoryInclusion P)
     (fun X Y =>
       ⟨(β_ X.1 Y.1).hom, (β_ X.1 Y.1).inv, (β_ X.1 Y.1).hom_inv_id, (β_ X.1 Y.1).inv_hom_id⟩)
-    fun X Y => by aesop_cat
+    fun X Y => by simp
 
 /-- The forgetful braided functor from a full braided subcategory into the original category
 ("forgetting" the condition).
diff --git a/Mathlib/CategoryTheory/NatIso.lean b/Mathlib/CategoryTheory/NatIso.lean
index e12d02fb99a67..caa4309d21b37 100644
--- a/Mathlib/CategoryTheory/NatIso.lean
+++ b/Mathlib/CategoryTheory/NatIso.lean
@@ -227,7 +227,7 @@ theorem ofComponents.app (app' : ∀ X : C, F.obj X ≅ G.obj X) (naturality) (X
 /-- A natural transformation is an isomorphism if all its components are isomorphisms.
 -/
 theorem isIso_of_isIso_app (α : F ⟶ G) [∀ X : C, IsIso (α.app X)] : IsIso α :=
-  (ofComponents (fun X => asIso (α.app X)) (by aesop)).isIso_hom
+  (ofComponents (fun X => asIso (α.app X)) (by simp)).isIso_hom
 
 /-- Horizontal composition of natural isomorphisms. -/
 @[simps]
diff --git a/Mathlib/CategoryTheory/Opposites.lean b/Mathlib/CategoryTheory/Opposites.lean
index 8cb8e3e027660..914d995a8d4cd 100644
--- a/Mathlib/CategoryTheory/Opposites.lean
+++ b/Mathlib/CategoryTheory/Opposites.lean
@@ -120,7 +120,7 @@ end
 
 /-- If `f` is an isomorphism, so is `f.op` -/
 instance isIso_op {X Y : C} (f : X ⟶ Y) [IsIso f] : IsIso f.op :=
-  ⟨⟨(inv f).op, ⟨Quiver.Hom.unop_inj (by aesop_cat), Quiver.Hom.unop_inj (by aesop_cat)⟩⟩⟩
+  ⟨⟨(inv f).op, ⟨Quiver.Hom.unop_inj (by simp), Quiver.Hom.unop_inj (by simp)⟩⟩⟩
 
 /-- If `f.op` is an isomorphism `f` must be too.
 (This cannot be an instance as it would immediately loop!)
diff --git a/Mathlib/CategoryTheory/Pi/Basic.lean b/Mathlib/CategoryTheory/Pi/Basic.lean
index 620eae9dd1af8..0b47b17e1e3a3 100644
--- a/Mathlib/CategoryTheory/Pi/Basic.lean
+++ b/Mathlib/CategoryTheory/Pi/Basic.lean
@@ -109,7 +109,7 @@ def comapComp (f : K → J) (g : J → I) : comap C g ⋙ comap (C ∘ g) f ≅
 /-- The natural isomorphism between pulling back then evaluating, and just evaluating. -/
 @[simps!]
 def comapEvalIsoEval (h : J → I) (j : J) : comap C h ⋙ eval (C ∘ h) j ≅ eval C (h j) :=
-  NatIso.ofComponents (fun _ => Iso.refl _) (by simp only [Iso.refl]; aesop_cat)
+  NatIso.ofComponents (fun _ => Iso.refl _) (by simp only [Iso.refl]; simp)
 
 end
 
diff --git a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
index 49104d0c125a5..4a9c75efd68f9 100644
--- a/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
+++ b/Mathlib/CategoryTheory/Preadditive/Biproducts.lean
@@ -143,7 +143,7 @@ def isBilimitOfIsLimit {f : J → C} (t : Bicone f) (ht : IsLimit t.toCone) : t.
 /-- We can turn any limit cone over a pair into a bilimit bicone. -/
 def biconeIsBilimitOfLimitConeOfIsLimit {f : J → C} {t : Cone (Discrete.functor f)}
     (ht : IsLimit t) : (Bicone.ofLimitCone ht).IsBilimit :=
-  isBilimitOfIsLimit _ <| IsLimit.ofIsoLimit ht <| Cones.ext (Iso.refl _) (by aesop_cat)
+  isBilimitOfIsLimit _ <| IsLimit.ofIsoLimit ht <| Cones.ext (Iso.refl _) (by simp)
 
 /-- In a preadditive category, any finite bicone which is a colimit cocone is in fact a bilimit
     bicone. -/
diff --git a/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean b/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
index c2f2f2b51b091..499eed7f4a959 100644
--- a/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
+++ b/Mathlib/CategoryTheory/Preadditive/OfBiproducts.lean
@@ -51,12 +51,12 @@ theorem isUnital_leftAdd : EckmannHilton.IsUnital (· +ₗ ·) 0 := by
   have hr : ∀ f : X ⟶ Y, biprod.lift (0 : X ⟶ Y) f = f ≫ biprod.inr := by
     intro f
     ext
-    · aesop_cat
+    · simp
     · simp [biprod.lift_fst, Category.assoc, biprod.inr_fst, comp_zero]
   have hl : ∀ f : X ⟶ Y, biprod.lift f (0 : X ⟶ Y) = f ≫ biprod.inl := by
     intro f
     ext
-    · aesop_cat
+    · simp
     · simp [biprod.lift_snd, Category.assoc, biprod.inl_snd, comp_zero]
   exact {
     left_id := fun f => by simp [hr f, leftAdd, Category.assoc, Category.comp_id, biprod.inr_desc],
@@ -67,12 +67,12 @@ theorem isUnital_rightAdd : EckmannHilton.IsUnital (· +ᵣ ·) 0 := by
   have h₂ : ∀ f : X ⟶ Y, biprod.desc (0 : X ⟶ Y) f = biprod.snd ≫ f := by
     intro f
     ext
-    · aesop_cat
+    · simp
     · simp only [biprod.inr_desc, BinaryBicone.inr_snd_assoc]
   have h₁ : ∀ f : X ⟶ Y, biprod.desc f (0 : X ⟶ Y) = biprod.fst ≫ f := by
     intro f
     ext
-    · aesop_cat
+    · simp
     · simp only [biprod.inr_desc, BinaryBicone.inr_fst_assoc, zero_comp]
   exact {
     left_id := fun f => by simp [h₂ f, rightAdd, biprod.lift_snd_assoc, Category.id_comp],
diff --git a/Mathlib/CategoryTheory/Simple.lean b/Mathlib/CategoryTheory/Simple.lean
index 619a1bdfe7847..3d1d618bb6c68 100644
--- a/Mathlib/CategoryTheory/Simple.lean
+++ b/Mathlib/CategoryTheory/Simple.lean
@@ -116,7 +116,7 @@ variable (C)
 
 /-- We don't want the definition of 'simple' to include the zero object, so we check that here. -/
 theorem zero_not_simple [Simple (0 : C)] : False :=
-  (Simple.mono_isIso_iff_nonzero (0 : (0 : C) ⟶ (0 : C))).mp ⟨⟨0, by aesop_cat⟩⟩ rfl
+  (Simple.mono_isIso_iff_nonzero (0 : (0 : C) ⟶ (0 : C))).mp ⟨⟨0, by simp⟩⟩ rfl
 
 end
 
diff --git a/Mathlib/CategoryTheory/SingleObj.lean b/Mathlib/CategoryTheory/SingleObj.lean
index a3e3ca9146610..48fed64ab7d7d 100644
--- a/Mathlib/CategoryTheory/SingleObj.lean
+++ b/Mathlib/CategoryTheory/SingleObj.lean
@@ -205,11 +205,11 @@ def toSingleObjEquiv (e : M ≃* N) : SingleObj M ≌ SingleObj N where
   unitIso := eqToIso (by
     rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
     congr 1
-    aesop_cat)
+    simp)
   counitIso := eqToIso (by
     rw [← MonoidHom.comp_toFunctor, ← MonoidHom.id_toFunctor]
     congr 1
-    aesop_cat)
+    simp)
 
 end MulEquiv
 
diff --git a/Mathlib/CategoryTheory/Sites/Pretopology.lean b/Mathlib/CategoryTheory/Sites/Pretopology.lean
index d888a2611acf2..bde2d0fb7bd77 100644
--- a/Mathlib/CategoryTheory/Sites/Pretopology.lean
+++ b/Mathlib/CategoryTheory/Sites/Pretopology.lean
@@ -172,7 +172,7 @@ def trivial : Pretopology C where
   pullbacks X Y f S := by
     rintro ⟨Z, g, i, rfl⟩
     refine ⟨pullback g f, pullback.snd _ _, ?_, ?_⟩
-    · refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by aesop_cat⟩⟩⟩
+    · refine ⟨⟨pullback.lift (f ≫ inv g) (𝟙 _) (by simp), ⟨?_, by simp⟩⟩⟩
       ext
       · rw [assoc, pullback.lift_fst, ← pullback.condition_assoc]
         simp
diff --git a/Mathlib/CategoryTheory/Sites/Subsheaf.lean b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
index be30cc3fa8ebc..421d09f0798b1 100644
--- a/Mathlib/CategoryTheory/Sites/Subsheaf.lean
+++ b/Mathlib/CategoryTheory/Sites/Subsheaf.lean
@@ -57,7 +57,7 @@ instance : PartialOrder (Subpresheaf F) :=
   PartialOrder.lift Subpresheaf.obj (fun _ _ => Subpresheaf.ext)
 
 instance : Top (Subpresheaf F) :=
-  ⟨⟨fun _ => ⊤, @fun U _ _ x _ => by aesop_cat⟩⟩
+  ⟨⟨fun _ => ⊤, @fun U _ _ x _ => by simp⟩⟩
 
 instance : Nonempty (Subpresheaf F) :=
   inferInstance
diff --git a/Mathlib/CategoryTheory/Square.lean b/Mathlib/CategoryTheory/Square.lean
index 1286c1bd87b9b..9062feb1d215c 100644
--- a/Mathlib/CategoryTheory/Square.lean
+++ b/Mathlib/CategoryTheory/Square.lean
@@ -172,9 +172,9 @@ commutative square `sq` to the obvious arrow from the left morphism of `sq`
 to the right morphism of `sq`. -/
 @[simps!]
 def toArrowArrowFunctor : Square C ⥤ Arrow (Arrow C) where
-  obj sq := Arrow.mk (Arrow.homMk sq.fac : Arrow.mk sq.f₁₃ ⟶ Arrow.mk sq.f₂₄)
-  map φ := Arrow.homMk (u := Arrow.homMk φ.comm₁₃.symm)
-    (v := Arrow.homMk φ.comm₂₄.symm) (by aesop_cat)
+  obj sq := Arrow.mk (Arrow.homMk _ _ sq.fac : Arrow.mk sq.f₁₃ ⟶ Arrow.mk sq.f₂₄)
+  map φ := Arrow.homMk (Arrow.homMk _ _ φ.comm₁₃.symm)
+    (Arrow.homMk _ _ φ.comm₂₄.symm)
 
 /-- The functor `Arrow (Arrow C) ⥤ Square C` which sends
 a morphism `Arrow.mk f ⟶ Arrow.mk g` to the commutative square
@@ -207,9 +207,9 @@ commutative square `sq` to the obvious arrow from the top morphism of `sq`
 to the bottom morphism of `sq`. -/
 @[simps!]
 def toArrowArrowFunctor' : Square C ⥤ Arrow (Arrow C) where
-  obj sq := Arrow.mk (Arrow.homMk sq.fac.symm : Arrow.mk sq.f₁₂ ⟶ Arrow.mk sq.f₃₄)
-  map φ := Arrow.homMk (u := Arrow.homMk φ.comm₁₂.symm)
-    (v := Arrow.homMk φ.comm₃₄.symm) (by aesop_cat)
+  obj sq := Arrow.mk (Arrow.homMk _ _ sq.fac.symm : Arrow.mk sq.f₁₂ ⟶ Arrow.mk sq.f₃₄)
+  map φ := Arrow.homMk (Arrow.homMk _ _ φ.comm₁₂.symm)
+    (Arrow.homMk _ _ φ.comm₃₄.symm)
 
 /-- The functor `Arrow (Arrow C) ⥤ Square C` which sends
 a morphism `Arrow.mk f ⟶ Arrow.mk g` to the commutative square
diff --git a/Mathlib/CategoryTheory/Subobject/Comma.lean b/Mathlib/CategoryTheory/Subobject/Comma.lean
index 20c1832042687..31c43bb091ef1 100644
--- a/Mathlib/CategoryTheory/Subobject/Comma.lean
+++ b/Mathlib/CategoryTheory/Subobject/Comma.lean
@@ -107,7 +107,7 @@ def subobjectEquiv [HasFiniteLimits C] [PreservesFiniteLimits T] (A : Structured
     refine ⟨fun h => Subobject.mk_le_mk_of_comm ?_ ?_, fun h => ?_⟩
     · exact homMk (Subobject.ofMkLEMk _ _ h)
         ((cancel_mono (T.map g.right)).1 (by simp [← T.map_comp]))
-    · aesop_cat
+    · simp
     · refine Subobject.mk_le_mk_of_comm (Subobject.ofMkLEMk _ _ h).right ?_
       exact congr_arg CommaMorphism.right (Subobject.ofMkLEMk_comp h)
 
@@ -187,7 +187,7 @@ theorem lift_projectQuotient [HasFiniteColimits C] [PreservesFiniteColimits S]
         · exact (Subobject.underlyingIso f.unop.left.op).unop
         · refine (cancel_epi (S.map f.unop.left)).1 ?_
           simpa [← Category.assoc, ← S.map_comp] using hq
-      · exact Quiver.Hom.unop_inj (by aesop_cat))
+      · exact Quiver.Hom.unop_inj (by simp))
 
 /-- Technical lemma for `quotientEquiv`. -/
 theorem unop_left_comp_ofMkLEMk_unop {A : CostructuredArrow S T} {P Q : (CostructuredArrow S T)ᵒᵖ}
diff --git a/Mathlib/CategoryTheory/Subobject/Lattice.lean b/Mathlib/CategoryTheory/Subobject/Lattice.lean
index 813f8887842b6..70d9b061a97da 100644
--- a/Mathlib/CategoryTheory/Subobject/Lattice.lean
+++ b/Mathlib/CategoryTheory/Subobject/Lattice.lean
@@ -59,7 +59,7 @@ variable [HasPullbacks C]
 is (isomorphic to) the top object in `MonoOver X`. -/
 def pullbackTop (f : X ⟶ Y) : (pullback f).obj ⊤ ≅ ⊤ :=
   iso_of_both_ways (leTop _)
-    (homMk (pullback.lift f (𝟙 _) (by aesop_cat)) (pullback.lift_snd _ _ _))
+    (homMk (pullback.lift f (𝟙 _) (by simp)) (pullback.lift_snd _ _ _))
 
 /-- There is a morphism from `⊤ : MonoOver A` to the pullback of a monomorphism along itself;
 as the category is thin this is an isomorphism. -/
@@ -527,7 +527,7 @@ def leInfCone {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s
             (by
               rcases j with ⟨-, ⟨g, ⟨m, rfl⟩⟩⟩
               simpa using m))))
-    (by aesop_cat)
+    (by simp)
 
 @[simp]
 theorem leInfCone_π_app_none {A : C} (s : Set (Subobject A)) (f : Subobject A)
@@ -572,7 +572,7 @@ theorem sInf_le {A : C} (s : Set (Subobject A)) (f) (hf : f ∈ s) : sInf s ≤
     simp only [Category.comp_id, Category.assoc, ← underlyingIso_hom_comp_eq_mk,
       Subobject.arrow_congr, congrArg_mpr_hom_left, Iso.cancel_iso_hom_left]
     convert limit.w (wideCospan s) (WidePullbackShape.Hom.term _)
-    aesop_cat
+    simp
 
 theorem le_sInf {A : C} (s : Set (Subobject A)) (f : Subobject A) (k : ∀ g ∈ s, f ≤ g) :
     f ≤ sInf s := by
diff --git a/Mathlib/CategoryTheory/Triangulated/Basic.lean b/Mathlib/CategoryTheory/Triangulated/Basic.lean
index e76c664d5f1d3..b8e3b05949917 100644
--- a/Mathlib/CategoryTheory/Triangulated/Basic.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Basic.lean
@@ -249,7 +249,7 @@ def binaryProductTriangleIsoBinaryBiproductTriangle
     (X₁ X₂ : C) [HasZeroMorphisms C] [HasBinaryBiproduct X₁ X₂] :
     binaryProductTriangle X₁ X₂ ≅ binaryBiproductTriangle X₁ X₂ :=
   Triangle.isoMk _ _ (Iso.refl _) (biprod.isoProd X₁ X₂).symm (Iso.refl _)
-    (by aesop_cat) (by aesop_cat) (by aesop_cat)
+    (by aesop_cat) (by simp) (by simp)
 
 section
 
diff --git a/Mathlib/CategoryTheory/Triangulated/Functor.lean b/Mathlib/CategoryTheory/Triangulated/Functor.lean
index c7c860c35beec..faa14d9b0ea07 100644
--- a/Mathlib/CategoryTheory/Triangulated/Functor.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Functor.lean
@@ -76,7 +76,7 @@ noncomputable def mapTriangleCommShiftIso (n : ℤ) :
     Triangle.shiftFunctor C n ⋙ F.mapTriangle ≅ F.mapTriangle ⋙ Triangle.shiftFunctor D n :=
   NatIso.ofComponents (fun T => Triangle.isoMk _ _
     ((F.commShiftIso n).app _) ((F.commShiftIso n).app _) ((F.commShiftIso n).app _)
-    (by aesop_cat) (by aesop_cat) (by
+    (by simp) (by simp) (by
       dsimp
       simp only [map_units_smul, map_comp, Linear.units_smul_comp, assoc,
         Linear.comp_units_smul, ← F.commShiftIso_hom_naturality_assoc]
@@ -103,7 +103,7 @@ def mapTriangleRotateIso :
   NatIso.ofComponents
     (fun T => Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
       ((F.commShiftIso (1 : ℤ)).symm.app _)
-      (by aesop_cat) (by aesop_cat) (by aesop_cat)) (by aesop_cat)
+      (by simp) (by simp) (by simp)) (by aesop_cat)
 
 /-- `F.mapTriangle` commutes with the inverse of the rotation of triangles. -/
 @[simps!]
@@ -112,7 +112,7 @@ noncomputable def mapTriangleInvRotateIso [F.Additive] :
       Pretriangulated.invRotate C ⋙ F.mapTriangle :=
   NatIso.ofComponents
     (fun T => Triangle.isoMk _ _ ((F.commShiftIso (-1 : ℤ)).symm.app _) (Iso.refl _) (Iso.refl _)
-      (by aesop_cat) (by aesop_cat) (by aesop_cat)) (by aesop_cat)
+      (by simp) (by simp) (by simp)) (by aesop_cat)
 
 
 variable (C) in
diff --git a/Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean b/Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
index 5e146b7317e28..dcec2c68e78ac 100644
--- a/Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Opposite/Pretriangulated.lean
@@ -88,7 +88,7 @@ noncomputable def contractibleTriangleIso (X : Cᵒᵖ) :
       rw [IsZero.iff_id_eq_zero]
       change (𝟙 ((0 : C)⟦(-1 : ℤ)⟧)).op = 0
       rw [← Functor.map_id, id_zero, Functor.map_zero, op_zero]))
-    (by aesop_cat) (by aesop_cat) (by aesop_cat)
+    (by simp) (by simp) (by simp)
 
 lemma contractible_distinguished (X : Cᵒᵖ) :
     contractibleTriangle X ∈ distinguishedTriangles C := by
@@ -103,7 +103,7 @@ noncomputable def rotateTriangleOpEquivalenceInverseObjRotateUnopIso (T : Triang
       ((triangleOpEquivalence C).inverse.obj T).unop :=
   Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _)
       (-((opShiftFunctorEquivalence C 1).unitIso.app T.obj₁).unop) (by simp)
-        (Quiver.Hom.op_inj (by aesop_cat)) (by aesop_cat)
+        (Quiver.Hom.op_inj (by simp)) (by simp)
 
 lemma rotate_distinguished_triangle (T : Triangle Cᵒᵖ) :
     T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C := by
@@ -119,7 +119,7 @@ lemma distinguished_cocone_triangle {X Y : Cᵒᵖ} (f : X ⟶ Y) :
     (shiftFunctor Cᵒᵖ (1 : ℤ)).map h.op, ?_⟩
   simp only [mem_distinguishedTriangles_iff]
   refine Pretriangulated.isomorphic_distinguished _ H _ ?_
-  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
+  exact Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
     (Quiver.Hom.op_inj (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))
 
 lemma complete_distinguished_triangle_morphism (T₁ T₂ : Triangle Cᵒᵖ)
diff --git a/Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean b/Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean
index cd0a07b4be3dd..2618748d4f279 100644
--- a/Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Opposite/Triangle.lean
@@ -73,7 +73,7 @@ equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ`
 @[simps!]
 noncomputable def unitIso : 𝟭 _ ≅ functor C ⋙ inverse C :=
   NatIso.ofComponents (fun T => Iso.op
-    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat)
+    (Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) (by simp) (by simp)
       (Quiver.Hom.op_inj
         (by simp [shift_unop_opShiftFunctorEquivalence_counitIso_inv_app]))))
     (fun {T₁ T₂} f => Quiver.Hom.unop_inj (by aesop_cat))
@@ -84,8 +84,8 @@ equivalence `triangleOpEquivalence C : (Triangle C)ᵒᵖ ≌ Triangle Cᵒᵖ`
 noncomputable def counitIso : inverse C ⋙ functor C ≅ 𝟭 _ :=
   NatIso.ofComponents (fun T => by
     refine Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _) ?_ ?_ ?_
-    · aesop_cat
-    · aesop_cat
+    · simp
+    · simp
     · dsimp
       rw [Functor.map_id, comp_id, id_comp, Functor.map_comp,
         ← opShiftFunctorEquivalence_counitIso_inv_naturality_assoc,
diff --git a/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean b/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
index c3b954b379632..1cbad40237ea8 100644
--- a/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
@@ -219,7 +219,7 @@ lemma contractible_distinguished₁ (X : C) :
   refine isomorphic_distinguished _
     (inv_rot_of_distTriang _ (contractible_distinguished X)) _ ?_
   exact Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _)
-    (by aesop_cat) (by aesop_cat) (by aesop_cat)
+    (by simp) (by simp) (by simp)
 
 /-- Obvious triangles `X ⟶ 0 ⟶ X⟦1⟧ ⟶ X⟦1⟧` are distinguished -/
 lemma contractible_distinguished₂ (X : C) :
@@ -227,7 +227,7 @@ lemma contractible_distinguished₂ (X : C) :
   refine isomorphic_distinguished _
     (inv_rot_of_distTriang _ (contractible_distinguished₁ (X⟦(1 : ℤ)⟧))) _ ?_
   exact Triangle.isoMk _ _ ((shiftEquiv C (1 : ℤ)).unitIso.app X) (Iso.refl _) (Iso.refl _)
-    (by aesop_cat) (by aesop_cat)
+    (by simp) (by simp)
     (by dsimp; simp only [shift_shiftFunctorCompIsoId_inv_app, id_comp])
 
 namespace Triangle
@@ -531,7 +531,7 @@ lemma binaryBiproductTriangle_distinguished (X₁ X₂ : C) :
   dsimp at he₁ he₂
   refine isomorphic_distinguished _ mem _ (Iso.symm ?_)
   refine Triangle.isoMk _ _ (Iso.refl _) e (Iso.refl _)
-    (by aesop_cat) (by aesop_cat) (by aesop_cat)
+    (by aesop_cat) (by aesop_cat) (by simp)
 
 lemma binaryProductTriangle_distinguished (X₁ X₂ : C) :
     binaryProductTriangle X₁ X₂ ∈ distTriang C :=
diff --git a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
index 22baf9e9ef9b8..f662bd84a092a 100644
--- a/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
+++ b/Mathlib/CategoryTheory/Triangulated/Subcategory.lean
@@ -81,7 +81,7 @@ def isoClosure : Subcategory C where
     exact le_isoClosure _ _
       (S.ext₂' (Triangle.mk (e₁.inv ≫ T.mor₁) (T.mor₂ ≫ e₃.hom) (e₃.inv ≫ T.mor₃ ≫ e₁.hom⟦1⟧'))
       (isomorphic_distinguished _ hT _
-        (Triangle.isoMk _ _ e₁.symm (Iso.refl _) e₃.symm (by aesop_cat) (by aesop_cat) (by
+        (Triangle.isoMk _ _ e₁.symm (Iso.refl _) e₃.symm (by simp) (by simp) (by
           dsimp
           simp only [assoc, Iso.cancel_iso_inv_left, ← Functor.map_comp, e₁.hom_inv_id,
             Functor.map_id, comp_id]))) h₁ h₃)
@@ -155,7 +155,7 @@ instance respectsIso_W : S.W.RespectsIso where
   precomp {X' X Y} e (he : IsIso e) := by
     rintro f ⟨Z, g, h, mem, mem'⟩
     refine ⟨Z, g, h ≫ inv e⟦(1 : ℤ)⟧', isomorphic_distinguished _ mem _ ?_, mem'⟩
-    refine Triangle.isoMk _ _ (asIso e) (Iso.refl _) (Iso.refl _) (by aesop_cat) (by aesop_cat) ?_
+    refine Triangle.isoMk _ _ (asIso e) (Iso.refl _) (Iso.refl _) (by simp) (by simp) ?_
     dsimp
     simp only [Functor.map_inv, assoc, IsIso.inv_hom_id, comp_id, id_comp]
   postcomp {X Y Y'} e (he : IsIso e) := by
diff --git a/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean b/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
index b811588238be2..c06cd41d963ae 100644
--- a/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
+++ b/Mathlib/CategoryTheory/Triangulated/TriangleShift.lean
@@ -65,7 +65,7 @@ noncomputable def Triangle.shiftFunctorZero : Triangle.shiftFunctor C 0 ≅ 𝟭
   NatIso.ofComponents
     (fun T => Triangle.isoMk _ _ ((CategoryTheory.shiftFunctorZero C ℤ).app _)
       ((CategoryTheory.shiftFunctorZero C ℤ).app _) ((CategoryTheory.shiftFunctorZero C ℤ).app _)
-      (by aesop_cat) (by aesop_cat) (by
+      (by simp) (by simp) (by
         dsimp
         simp only [one_smul, assoc, shiftFunctorComm_zero_hom_app,
           ← Functor.map_comp, Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id,
@@ -109,7 +109,7 @@ noncomputable def rotateRotateRotateIso :
     rotate C ⋙ rotate C ⋙ rotate C ≅ Triangle.shiftFunctor C 1 :=
   NatIso.ofComponents
     (fun T => Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _)
-      (by aesop_cat) (by aesop_cat) (by aesop_cat))
+      (by simp) (by simp) (by simp))
     (by aesop_cat)
 
 /-- Rotating triangles three times backwards identifies with the shift by `-1`. -/
@@ -117,8 +117,8 @@ noncomputable def invRotateInvRotateInvRotateIso :
     invRotate C ⋙ invRotate C ⋙ invRotate C ≅ Triangle.shiftFunctor C (-1) :=
   NatIso.ofComponents
     (fun T => Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _)
-      (by aesop_cat)
-      (by aesop_cat)
+      (by simp)
+      (by simp)
       (by
         dsimp [shiftFunctorCompIsoId]
         simp [shiftFunctorComm_eq C _ _ _ (add_neg_cancel (1 : ℤ))]))
diff --git a/Mathlib/CategoryTheory/Yoneda.lean b/Mathlib/CategoryTheory/Yoneda.lean
index 05d0c28efabb3..e362440ade3cf 100644
--- a/Mathlib/CategoryTheory/Yoneda.lean
+++ b/Mathlib/CategoryTheory/Yoneda.lean
@@ -523,7 +523,7 @@ def yonedaCompUliftFunctorEquiv (F : Cᵒᵖ ⥤ Type max v₁ w) (X : C) :
     dsimp
     rw [Category.comp_id]
     rfl
-  right_inv f := by aesop_cat
+  right_inv f := by simp
 
 /-- The Yoneda lemma asserts that the Yoneda pairing
 `(X : Cᵒᵖ, F : Cᵒᵖ ⥤ Type) ↦ (yoneda.obj (unop X) ⟶ F)`
@@ -705,7 +705,7 @@ def coyonedaCompUliftFunctorEquiv (F : C ⥤ Type max v₁ w) (X : Cᵒᵖ) :
     dsimp
     rw [Category.id_comp]
     rfl
-  right_inv f := by aesop_cat
+  right_inv f := by simp
 
 /-- The Coyoneda lemma asserts that the Coyoneda pairing
 `(X : C, F : C ⥤ Type) ↦ (coyoneda.obj X ⟶ F)`
diff --git a/Mathlib/Combinatorics/Enumerative/Partition.lean b/Mathlib/Combinatorics/Enumerative/Partition.lean
index b2226025ed657..bdc8edeb9c657 100644
--- a/Mathlib/Combinatorics/Enumerative/Partition.lean
+++ b/Mathlib/Combinatorics/Enumerative/Partition.lean
@@ -54,12 +54,11 @@ structure Partition (n : ℕ) where
   parts_pos : ∀ {i}, i ∈ parts → 0 < i
   /-- proof that the `parts` sum to `n`-/
   parts_sum : parts.sum = n
-  -- Porting note: chokes on `parts_pos`
-  --deriving DecidableEq
+deriving DecidableEq
 
 namespace Partition
 
--- TODO: This should be automatically derived, see https://github.com/leanprover/lean4/issues/2914
+@[deprecated "Partition now derives an instance of DecidableEq." (since := "2024-12-28")]
 instance decidableEqPartition {n : ℕ} : DecidableEq (Partition n) :=
   fun _ _ => decidable_of_iff' _ Partition.ext_iff
 
diff --git a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
index 7cd217fadb8cf..0031c9b006e43 100644
--- a/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
+++ b/Mathlib/Computability/AkraBazzi/AkraBazzi.lean
@@ -843,7 +843,7 @@ lemma isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0)
           (fun z => z ^ (p-1) / (log z ^ 2)) =o[atTop] fun z => z ^ (p-1) / 1 := by
                       simp_rw [div_eq_mul_inv]
                       refine IsBigO.mul_isLittleO (isBigO_refl _ _)
-                        (IsLittleO.inv_rev ?_ (by aesop (add safe Eventually.of_forall)))
+                        (IsLittleO.inv_rev ?_ (by simp))
                       rw [isLittleO_const_left]
                       refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
                       exact Tendsto.comp (g := fun z => z ^ 2)
@@ -867,7 +867,7 @@ lemma isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0)
           (fun z => -(z ^ (p-1) / (log z ^ 2))) =o[atTop] fun z => z ^ (p-1) / 1 := by
                       simp_rw [isLittleO_neg_left, div_eq_mul_inv]
                       refine IsBigO.mul_isLittleO (isBigO_refl _ _)
-                        (IsLittleO.inv_rev ?_ (by aesop (add safe Eventually.of_forall)))
+                        (IsLittleO.inv_rev ?_ (by simp))
                       rw [isLittleO_const_left]
                       refine Or.inr <| Tendsto.comp tendsto_norm_atTop_atTop ?_
                       exact Tendsto.comp (g := fun z => z ^ 2)
diff --git a/Mathlib/Data/MLList/BestFirst.lean b/Mathlib/Data/MLList/BestFirst.lean
index 430ac91fa3323..4f0ae77aca908 100644
--- a/Mathlib/Data/MLList/BestFirst.lean
+++ b/Mathlib/Data/MLList/BestFirst.lean
@@ -307,7 +307,7 @@ variable {m : Type → Type} {α : Type} [Monad m] [Alternative m] [LinearOrder
 for simple use cases. -/
 local instance instOrderBotEq {a : α} : OrderBot { x : α // x = a } where
   bot := ⟨a, rfl⟩
-  bot_le := by aesop
+  bot_le := by simp
 
 /--
 A lazy list recording the best first search of a graph generated by a function
diff --git a/Mathlib/Data/Matrix/ColumnRowPartitioned.lean b/Mathlib/Data/Matrix/ColumnRowPartitioned.lean
index c583ebb1d3b5e..d4d5448a54f8f 100644
--- a/Mathlib/Data/Matrix/ColumnRowPartitioned.lean
+++ b/Mathlib/Data/Matrix/ColumnRowPartitioned.lean
@@ -125,8 +125,7 @@ lemma fromRows_toRows (A : Matrix (m₁ ⊕ m₂) n R) : fromRows A.toRows₁ A.
 
 lemma fromRows_inj : Function.Injective2 (@fromRows R m₁ m₂ n) := by
   intros x1 x2 y1 y2
-  simp only [funext_iff, ← Matrix.ext_iff]
-  aesop
+  simp [← Matrix.ext_iff]
 
 lemma fromCols_inj : Function.Injective2 (@fromCols R m n₁ n₂) := by
   intros x1 x2 y1 y2
diff --git a/Mathlib/Data/Matroid/Closure.lean b/Mathlib/Data/Matroid/Closure.lean
index cb14ccdda92a3..534a3d8ddbc12 100644
--- a/Mathlib/Data/Matroid/Closure.lean
+++ b/Mathlib/Data/Matroid/Closure.lean
@@ -154,7 +154,7 @@ lemma closure_subset_ground (M : Matroid α) (X : Set α) : M.closure X ⊆ M.E
   simp_rw [closure_def, inter_assoc, inter_self]
 
 lemma inter_ground_subset_closure (M : Matroid α) (X : Set α) : X ∩ M.E ⊆ M.closure X := by
-  simp_rw [closure_def, subset_sInter_iff]; aesop
+  simp_rw [closure_def, subset_sInter_iff]; simp
 
 lemma mem_closure_iff_forall_mem_flat (X : Set α) (hX : X ⊆ M.E := by aesop_mat) :
     e ∈ M.closure X ↔ ∀ F, M.Flat F → X ⊆ F → e ∈ F := by
diff --git a/Mathlib/Data/PFunctor/Multivariate/M.lean b/Mathlib/Data/PFunctor/Multivariate/M.lean
index cb6ed15fd11ac..3760a1050ad44 100644
--- a/Mathlib/Data/PFunctor/Multivariate/M.lean
+++ b/Mathlib/Data/PFunctor/Multivariate/M.lean
@@ -284,7 +284,7 @@ theorem M.bisim' {α : TypeVec n} (R : P.M α → P.M α → Prop)
     induction Hr
     · rw [← Quot.factor_mk_eq R (Relation.EqvGen R) this]
       rwa [appendFun_comp_id, ← MvFunctor.map_map, ← MvFunctor.map_map, h]
-    all_goals aesop
+    all_goals simp_all
 
 theorem M.dest_map {α β : TypeVec n} (g : α ⟹ β) (x : P.M α) :
     M.dest P (g <$$> x) = (appendFun g fun x => g <$$> x) <$$> M.dest P x := by
diff --git a/Mathlib/Data/Part.lean b/Mathlib/Data/Part.lean
index 842a941412357..98ebf824ed437 100644
--- a/Mathlib/Data/Part.lean
+++ b/Mathlib/Data/Part.lean
@@ -397,7 +397,7 @@ theorem assert_pos {p : Prop} {f : p → Part α} (h : p) : assert p f = f h :=
   simp only [h', mk.injEq, h, exists_prop_of_true, true_and]
   apply Function.hfunext
   · simp only [h, h', exists_prop_of_true]
-  · aesop
+  · simp
 
 theorem assert_neg {p : Prop} {f : p → Part α} (h : ¬p) : assert p f = none := by
   dsimp [assert, none]; congr
diff --git a/Mathlib/Data/Set/Pointwise/SMul.lean b/Mathlib/Data/Set/Pointwise/SMul.lean
index 4a60e0e49e98f..84372884b6f19 100644
--- a/Mathlib/Data/Set/Pointwise/SMul.lean
+++ b/Mathlib/Data/Set/Pointwise/SMul.lean
@@ -202,6 +202,11 @@ theorem image_smul_distrib [MulOneClass α] [MulOneClass β] [FunLike F α β] [
     f '' (a • s) = f a • f '' s :=
   image_comm <| map_mul _ _
 
+open scoped RightActions in
+@[to_additive]
+lemma image_op_smul_distrib [MulOneClass α] [MulOneClass β] [FunLike F α β] [MonoidHomClass F α β]
+    (f : F) (a : α) (s : Set α) : f '' (s <• a) = f '' s <• f a := image_comm fun _ ↦ map_mul _ _ _
+
 section SMul
 
 variable [SMul αᵐᵒᵖ β] [SMul β γ] [SMul α γ]
diff --git a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
index edc1b664e2ba8..45478ac73f241 100644
--- a/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
+++ b/Mathlib/Geometry/RingedSpace/LocallyRingedSpace/HasColimits.lean
@@ -82,7 +82,7 @@ noncomputable def coproductCofan : Cocone F where
   ι :=
     { app := fun j => ⟨colimit.ι (C := SheafedSpace.{u+1, u, u} CommRingCatMax.{u, u})
         (F ⋙ forgetToSheafedSpace) j, inferInstance⟩
-      naturality := fun ⟨j⟩ ⟨j'⟩ ⟨⟨(f : j = j')⟩⟩ => by subst f; aesop }
+      naturality := fun ⟨j⟩ ⟨j'⟩ ⟨⟨(f : j = j')⟩⟩ => by subst f; simp }
 
 /-- The explicit coproduct cofan constructed in `coproduct_cofan` is indeed a colimit. -/
 noncomputable def coproductCofanIsColimit : IsColimit (coproductCofan F) where
diff --git a/Mathlib/GroupTheory/SpecificGroups/KleinFour.lean b/Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
index e5a725fd32218..2ad3ed38cd7f4 100644
--- a/Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/KleinFour.lean
@@ -113,7 +113,7 @@ lemma eq_finset_univ [Fintype G] [DecidableEq G]
   rw [card_four']
   repeat rw [card_insert_of_not_mem]
   on_goal 4 => simpa using mul_not_mem_of_exponent_two (by simp) hx hy hxy
-  all_goals aesop
+  all_goals simp_all
 
 @[to_additive]
 lemma eq_mul_of_ne_all {x y z : G} (hx : x ≠ 1)
diff --git a/Mathlib/LinearAlgebra/FreeProduct/Basic.lean b/Mathlib/LinearAlgebra/FreeProduct/Basic.lean
index a6d1297916a19..15dd2e3d55456 100644
--- a/Mathlib/LinearAlgebra/FreeProduct/Basic.lean
+++ b/Mathlib/LinearAlgebra/FreeProduct/Basic.lean
@@ -189,7 +189,7 @@ theorem mul_injections (a₁ a₂ : A i) :
     ι' R A (DirectSum.lof R I A i a₁) * ι' R A (DirectSum.lof R I A i a₂)
       = ι' R A (DirectSum.lof R I A i (a₁ * a₂)) := by
   convert RingQuot.mkAlgHom_rel R <| rel.prod
-  aesop
+  simp
 
 /--The `i`th canonical injection, from `A i` to the free product, as
 a linear map.-/
diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
index fd7f09efc5db7..2a0d1fc752546 100644
--- a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
+++ b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
@@ -241,8 +241,8 @@ theorem nontrivial_of_invariantBasisNumber : Nontrivial R := by
   exact
     { toFun := 0
       invFun := 0
-      map_add' := by aesop
-      map_smul' := by aesop
+      map_add' := by simp
+      map_smul' := by simp
       left_inv := fun _ => by simp [eq_iff_true_of_subsingleton]
       right_inv := fun _ => by simp [eq_iff_true_of_subsingleton] }
 
diff --git a/Mathlib/LinearAlgebra/Multilinear/Basic.lean b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
index 5de11b6d8fc35..f4fa630b71b58 100644
--- a/Mathlib/LinearAlgebra/Multilinear/Basic.lean
+++ b/Mathlib/LinearAlgebra/Multilinear/Basic.lean
@@ -1081,8 +1081,8 @@ map from `Π i, M₁ᵢ ⟶ M₁ᵢ'` to `M ⟶ M₂` via `(fᵢ) ↦ v ↦ g(f
     MultilinearMap R M₁' M₂ →ₗ[R]
     MultilinearMap R (fun i ↦ M₁ i →ₗ[R] M₁' i) (MultilinearMap R M₁ M₂) where
   toFun g := (LinearMap.applyₗ g).compMultilinearMap compLinearMapMultilinear
-  map_add' := by aesop
-  map_smul' := by aesop
+  map_add' := by simp
+  map_smul' := by simp
 
 end
 
diff --git a/Mathlib/LinearAlgebra/Reflection.lean b/Mathlib/LinearAlgebra/Reflection.lean
index 7201b2603f574..612afa9e70760 100644
--- a/Mathlib/LinearAlgebra/Reflection.lean
+++ b/Mathlib/LinearAlgebra/Reflection.lean
@@ -311,10 +311,11 @@ This rather technical-looking lemma exists because it is exactly what is needed
 uniqueness results for root data / systems. One might regard this lemma as lying at the boundary of
 linear algebra and combinatorics since the finiteness assumption is the key. -/
 lemma Dual.eq_of_preReflection_mapsTo [CharZero R] [NoZeroSMulDivisors R M]
-    {x : M} (hx : x ≠ 0) {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : span R Φ = ⊤) {f g : Dual R M}
+    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hΦ₂ : span R Φ = ⊤) {f g : Dual R M}
     (hf₁ : f x = 2) (hf₂ : MapsTo (preReflection x f) Φ Φ)
     (hg₁ : g x = 2) (hg₂ : MapsTo (preReflection x g) Φ Φ) :
     f = g := by
+  have hx : x ≠ 0 := by rintro rfl; simp at hf₁
   let u := reflection hg₁ * reflection hf₁
   have hu : u = LinearMap.id (R := R) (M := M) + (f - g).smulRight x := by
     ext y
@@ -344,7 +345,7 @@ lemma Dual.eq_of_preReflection_mapsTo [CharZero R] [NoZeroSMulDivisors R M]
 uniqueness result for root data. See the doc string of `Module.Dual.eq_of_preReflection_mapsTo` for
 further remarks. -/
 lemma Dual.eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M]
-    {x : M} (hx : x ≠ 0) {Φ : Set M} (hΦ₁ : Φ.Finite) (hx' : x ∈ span R Φ) {f g : Dual R M}
+    {x : M} {Φ : Set M} (hΦ₁ : Φ.Finite) (hx : x ∈ span R Φ) {f g : Dual R M}
     (hf₁ : f x = 2) (hf₂ : MapsTo (preReflection x f) Φ Φ)
     (hg₁ : g x = 2) (hg₂ : MapsTo (preReflection x g) Φ Φ) :
     (span R Φ).subtype.dualMap f = (span R Φ).subtype.dualMap g := by
@@ -355,8 +356,7 @@ lemma Dual.eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M]
     simp only [Φ']
     rw [range_inclusion]
     simp
-  let x' : span R Φ := ⟨x, hx'⟩
-  have hx' : x' ≠ 0 := Subtype.coe_ne_coe.1 hx
+  let x' : span R Φ := ⟨x, hx⟩
   have this : ∀ {F : Dual R M}, MapsTo (preReflection x F) Φ Φ →
       MapsTo (preReflection x' ((span R Φ).subtype.dualMap F)) Φ' Φ' := by
     intro F hF ⟨y, hy⟩ hy'
@@ -365,7 +365,7 @@ lemma Dual.eq_of_preReflection_mapsTo' [CharZero R] [NoZeroSMulDivisors R M]
     simp only [SetLike.coe_sort_coe, mem_setOf_eq] at hy' ⊢
     rw [range_inclusion]
     exact hF hy'
-  exact eq_of_preReflection_mapsTo hx' hΦ'₁ hΦ'₂ hf₁ (this hf₂) hg₁ (this hg₂)
+  exact eq_of_preReflection_mapsTo hΦ'₁ hΦ'₂ hf₁ (this hf₂) hg₁ (this hg₂)
 
 variable {y}
 variable {g : Dual R M}
diff --git a/Mathlib/LinearAlgebra/RootSystem/Basic.lean b/Mathlib/LinearAlgebra/RootSystem/Basic.lean
index ba9290e8307a8..749ec3364bcb0 100644
--- a/Mathlib/LinearAlgebra/RootSystem/Basic.lean
+++ b/Mathlib/LinearAlgebra/RootSystem/Basic.lean
@@ -135,7 +135,7 @@ protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
   ext i
   apply P₁.injOn_dualMap_subtype_span_root_coroot (mem_range_self i) (hc ▸ mem_range_self i)
   simp only [LinearMap.coe_comp, LinearEquiv.coe_coe, comp_apply]
-  apply Dual.eq_of_preReflection_mapsTo' (P₁.ne_zero i) (finite_range P₁.root)
+  apply Dual.eq_of_preReflection_mapsTo' (finite_range P₁.root)
   · exact Submodule.subset_span (mem_range_self i)
   · exact P₁.coroot_root_two i
   · exact P₁.mapsTo_reflection_root i
@@ -177,7 +177,7 @@ private lemma coroot_eq_coreflection_of_root_eq' [CharZero R] [NoZeroSMulDivisor
   have := injOn_dualMap_subtype_span_range_range (finite_range root)
     (c := p.flip ∘ coroot) hp hr
   apply this (mem_range_self k) (mem_range_self l)
-  refine Dual.eq_of_preReflection_mapsTo' hk₀ (finite_range root)
+  refine Dual.eq_of_preReflection_mapsTo' (finite_range root)
     (Submodule.subset_span <| mem_range_self k) (hp k) (hr k) hkl ?_
   rw [comp_apply, hl, hk, hij]
   exact (hr i).comp <| (hr j).comp (hr i)
@@ -232,7 +232,7 @@ protected lemma ext [CharZero R] [NoZeroSMulDivisors R M]
   rintro P₁ P₂ he hr - ⟨i, rfl⟩
   use i
   apply P₁.bijectiveRight.injective
-  apply Dual.eq_of_preReflection_mapsTo (P₁.ne_zero i) (finite_range P₁.root) P₁.span_eq_top
+  apply Dual.eq_of_preReflection_mapsTo (finite_range P₁.root) P₁.span_eq_top
   · exact hr ▸ he ▸ P₂.coroot_root_two i
   · exact hr ▸ he ▸ P₂.mapsTo_reflection_root i
   · exact P₁.coroot_root_two i
@@ -261,7 +261,7 @@ private lemma coroot_eq_coreflection_of_root_eq_of_span_eq_top [CharZero R] [NoZ
       preReflection_apply] -- v4.7.0-rc1 issues
   have hk₀ : root k ≠ 0 := fun h ↦ by simpa [h, ← PerfectPairing.toLin_apply] using hp k
   apply p.bijectiveRight.injective
-  apply Dual.eq_of_preReflection_mapsTo hk₀ (finite_range root) hsp (hp k) (hs k)
+  apply Dual.eq_of_preReflection_mapsTo (finite_range root) hsp (hp k) (hs k)
   · simp [map_sub, α, β, α', β', sα, sβ, sα', hk, preReflection_apply, hp i, hp j, mul_two,
       mul_comm (p α β')]
     ring -- v4.7.0-rc1 issues
diff --git a/Mathlib/LinearAlgebra/Semisimple.lean b/Mathlib/LinearAlgebra/Semisimple.lean
index c7032628a6166..feb4bde80dc93 100644
--- a/Mathlib/LinearAlgebra/Semisimple.lean
+++ b/Mathlib/LinearAlgebra/Semisimple.lean
@@ -73,8 +73,7 @@ lemma isSemisimple_iff' :
 
 lemma isSemisimple_iff :
     f.IsSemisimple ↔ ∀ p ∈ invtSubmodule f, ∃ q ∈ invtSubmodule f, IsCompl p q := by
-  simp_rw [isSemisimple_iff']
-  aesop
+  simp [isSemisimple_iff']
 
 lemma isSemisimple_restrict_iff (p) (hp : p ∈ invtSubmodule f) :
     IsSemisimple (LinearMap.restrict f hp) ↔
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
index 21ad44e035faf..0c8559a3153a9 100644
--- a/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
+++ b/Mathlib/LinearAlgebra/TensorProduct/Quotient.lean
@@ -107,7 +107,7 @@ noncomputable def quotientTensorEquiv (m : Submodule R M) :
     erw [Submodule.map_id, Submodule.map_id]
     simp only [sup_eq_left]
     rw [map_range_eq_span_tmul, map_range_eq_span_tmul]
-    aesop)
+    simp)
 
 @[simp]
 lemma quotientTensorEquiv_apply_tmul_mk (m : Submodule R M) (x : M) (y : N) :
@@ -137,7 +137,7 @@ noncomputable def tensorQuotientEquiv (n : Submodule R N) :
     erw [Submodule.map_id, Submodule.map_id]
     simp only [sup_eq_right]
     rw [map_range_eq_span_tmul, map_range_eq_span_tmul]
-    aesop)
+    simp)
 
 @[simp]
 lemma tensorQuotientEquiv_apply_mk_tmul (n : Submodule R N) (x : M) (y : N) :
diff --git a/Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean b/Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
index 6e2b5cedfb464..41ac33f231c08 100644
--- a/Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
+++ b/Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
@@ -69,6 +69,11 @@ theorem ae_const_le_iff_forall_lt_measure_zero {β} [LinearOrder β] [Topologica
   intro n
   exact hc _ (u_lt n)
 
+lemma ae_le_const_iff_forall_gt_measure_zero {β} [LinearOrder β] [TopologicalSpace β]
+    [OrderTopology β] [FirstCountableTopology β] {μ : Measure α} (f : α → β) (c : β) :
+    (∀ᵐ x ∂μ, f x ≤ c) ↔ ∀ b, c < b → μ {x | b ≤ f x} = 0 :=
+  ae_const_le_iff_forall_lt_measure_zero (β := βᵒᵈ) _ _
+
 theorem ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ [SigmaFinite μ]
     {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
     (h : ∀ s, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ ≤ ∫⁻ x in s, g x ∂μ) :
diff --git a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean
index caed697da9d50..65acdbcc140ed 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/Basic.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/Basic.lean
@@ -590,33 +590,52 @@ inner regular Haar measures (and in particular for any Haar measure on a second
 
 open Pointwise
 
-/-- **Steinhaus Theorem** In any locally compact group `G` with an inner regular Haar measure `μ`,
+@[to_additive]
+private lemma steinhaus_mul_aux (μ : Measure G) [IsHaarMeasure μ] [μ.InnerRegularCompactLTTop]
+    [LocallyCompactSpace G] (E : Set G) (hE : MeasurableSet E)
+    (hEapprox : ∃ K ⊆ E, IsCompact K ∧ 0 < μ K) : E / E ∈ 𝓝 (1 : G) := by
+  /- For any measure `μ` and set `E` containing a compact set `K` of positive measure, there exists
+  a neighborhood `V` of the identity such that `v • K \ K` has small measure for all `v ∈ V`, say
+  `< μ K`. Then `v • K` and `K` can not be disjoint, as otherwise `μ (v • K \ K) = μ (v • K) = μ K`.
+  This show that `K / K` contains the neighborhood `V` of `1`, and therefore that it is
+  itself such a neighborhood. -/
+  obtain ⟨K, hKE, hK, K_closed, hKpos⟩ : ∃ K ⊆ E, IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
+    obtain ⟨K, hKE, hK_comp, hK_meas⟩ := hEapprox
+    exact ⟨closure K, hK_comp.closure_subset_measurableSet hE hKE, hK_comp.closure,
+      isClosed_closure, by rwa [hK_comp.measure_closure]⟩
+  filter_upwards [eventually_nhds_one_measure_smul_diff_lt hK K_closed hKpos.ne' (μ := μ)] with g hg
+  obtain ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩ : ∃ x ∈ g • K, x ∈ K :=
+     not_disjoint_iff.1 fun hd ↦ by simp [hd.symm.sdiff_eq_right, measure_smul] at hg
+  simpa using div_mem_div (hKE hgxK) (hKE hxK)
+
+/-- **Steinhaus Theorem** for finite mass sets.
+
+In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure
+sets, for any measurable set `E` of finite positive measure, the set `E / E` is a neighbourhood of
+`1`. -/
+@[to_additive
+"**Steinhaus Theorem** for finite mass sets.
+
+In any locally compact group `G` with an Haar measure `μ` that's inner regular on finite measure
+sets, for any measurable set `E` of finite positive measure, the set `E - E` is a neighbourhood of
+`0`. "]
+theorem div_mem_nhds_one_of_haar_pos_ne_top (μ : Measure G) [IsHaarMeasure μ]
+    [LocallyCompactSpace G] [μ.InnerRegularCompactLTTop] (E : Set G) (hE : MeasurableSet E)
+    (hEpos : 0 < μ E) (hEfin : μ E ≠ ∞) : E / E ∈ 𝓝 (1 : G) :=
+  steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact_of_ne_top hEfin hEpos
+
+/-- **Steinhaus Theorem**.
+
+In any locally compact group `G` with an inner regular Haar measure `μ`,
 for any measurable set `E` of positive measure, the set `E / E` is a neighbourhood of `1`. -/
 @[to_additive
-"**Steinhaus Theorem** In any locally compact group `G` with an inner regular Haar measure `μ`,
+"**Steinhaus Theorem**.
+
+In any locally compact group `G` with an inner regular Haar measure `μ`,
 for any measurable set `E` of positive measure, the set `E - E` is a neighbourhood of `0`."]
 theorem div_mem_nhds_one_of_haar_pos (μ : Measure G) [IsHaarMeasure μ] [LocallyCompactSpace G]
     [InnerRegular μ] (E : Set G) (hE : MeasurableSet E) (hEpos : 0 < μ E) :
-    E / E ∈ 𝓝 (1 : G) := by
-  /- For any inner regular measure `μ` and set `E` of positive measure, we can find a compact
-    set `K` of positive measure inside `E`. Further, there exists a neighborhood `V` of the
-    identity such that `v • K \ K` has small measure for all `v ∈ V`, say `< μ K`.
-    Then `v • K` and `K` can not be disjoint, as otherwise `μ (v • K \ K) = μ (v • K) = μ K`.
-    This show that `K / K` contains the neighborhood `V` of `1`, and therefore that it is
-    itself such a neighborhood. -/
-  obtain ⟨K, hKE, hK, K_closed, hKpos⟩ :
-      ∃ (K : Set G), K ⊆ E ∧ IsCompact K ∧ IsClosed K ∧ 0 < μ K := by
-    rcases MeasurableSet.exists_lt_isCompact hE hEpos with ⟨K, KE, K_comp, K_meas⟩
-    refine ⟨closure K, ?_, K_comp.closure, isClosed_closure, ?_⟩
-    · exact K_comp.closure_subset_measurableSet hE KE
-    · rwa [K_comp.measure_closure]
-  filter_upwards [eventually_nhds_one_measure_smul_diff_lt hK K_closed hKpos.ne' (μ := μ)] with g hg
-  have : ¬Disjoint (g • K) K := fun hd ↦ by
-    rw [hd.symm.sdiff_eq_right, measure_smul] at hg
-    exact hg.false
-  rcases Set.not_disjoint_iff.1 this with ⟨_, ⟨x, hxK, rfl⟩, hgxK⟩
-  simpa using div_mem_div (hKE hgxK) (hKE hxK)
-
+    E / E ∈ 𝓝 (1 : G) := steinhaus_mul_aux μ E hE <| hE.exists_lt_isCompact hEpos
 
 section SecondCountable_SigmaFinite
 /-! In this section, we investigate uniqueness of left-invariant measures without assuming that
diff --git a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
index dc9e9ec5eeea0..c52acf767b115 100644
--- a/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/Haar/NormedSpace.lean
@@ -14,12 +14,9 @@ import Mathlib.MeasureTheory.Integral.SetIntegral
 
 noncomputable section
 
+open Function Filter Inv MeasureTheory.Measure Module Set TopologicalSpace
 open scoped NNReal ENNReal Pointwise Topology
 
-open Inv Set Function MeasureTheory.Measure Filter
-
-open Module
-
 namespace MeasureTheory
 
 namespace Measure
@@ -44,6 +41,34 @@ instance MapLinearEquiv.isAddHaarMeasure (e : G ≃ₗ[𝕜] H) : IsAddHaarMeasu
 
 end LinearEquiv
 
+section SeminormedGroup
+variable {G H : Type*} [MeasurableSpace G] [Group G] [TopologicalSpace G]
+  [TopologicalGroup G] [BorelSpace G] [LocallyCompactSpace G]
+  [MeasurableSpace H] [SeminormedGroup H] [OpensMeasurableSpace H]
+
+-- TODO: This could be streamlined by proving that inner regular always exist
+open Metric Bornology in
+@[to_additive]
+lemma _root_.MonoidHom.exists_nhds_isBounded (f : G →* H) (hf : Measurable f) (x : G) :
+    ∃ s ∈ 𝓝 x, IsBounded (f '' s) := by
+  let K : PositiveCompacts G := Classical.arbitrary _
+  obtain ⟨n, hn⟩ : ∃ n : ℕ, 0 < haar (interior K ∩ f ⁻¹' ball 1 n) := by
+    by_contra!
+    simp_rw [nonpos_iff_eq_zero, ← measure_iUnion_null_iff, ← inter_iUnion, ← preimage_iUnion,
+      iUnion_ball_nat, preimage_univ, inter_univ] at this
+    exact this.not_gt <| isOpen_interior.measure_pos _ K.interior_nonempty
+  rw [← one_mul x, ← op_smul_eq_mul]
+  refine ⟨_, smul_mem_nhds_smul _ <| div_mem_nhds_one_of_haar_pos_ne_top haar _
+    (isOpen_interior.measurableSet.inter <| hf measurableSet_ball) hn <|
+      mt (measure_mono_top <| inter_subset_left.trans interior_subset) K.isCompact.measure_ne_top,
+    ?_⟩
+  have : Bornology.IsBounded (f '' (interior K ∩ f ⁻¹' ball 1 n)) :=
+    isBounded_ball.subset <| (image_mono inter_subset_right).trans <| image_preimage_subset _ _
+  rw [image_op_smul_distrib, image_div]
+  exact (this.div this).smul _
+
+end SeminormedGroup
+
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E]
   [FiniteDimensional ℝ E] (μ : Measure E) [IsAddHaarMeasure μ] {F : Type*} [NormedAddCommGroup F]
   [NormedSpace ℝ F]
diff --git a/Mathlib/ModelTheory/ElementaryMaps.lean b/Mathlib/ModelTheory/ElementaryMaps.lean
index 6b3b1c267638e..b044135204fda 100644
--- a/Mathlib/ModelTheory/ElementaryMaps.lean
+++ b/Mathlib/ModelTheory/ElementaryMaps.lean
@@ -138,14 +138,14 @@ theorem map_constants (φ : M ↪ₑ[L] N) (c : L.Constants) : φ c = c :=
 def toEmbedding (f : M ↪ₑ[L] N) : M ↪[L] N where
   toFun := f
   inj' := f.injective
-  map_fun' {_} f x := by aesop
-  map_rel' {_} R x := by aesop
+  map_fun' {_} f x := by simp
+  map_rel' {_} R x := by simp
 
 /-- An elementary embedding is also a first-order homomorphism. -/
 def toHom (f : M ↪ₑ[L] N) : M →[L] N where
   toFun := f
-  map_fun' {_} f x := by aesop
-  map_rel' {_} R x := by aesop
+  map_fun' {_} f x := by simp
+  map_rel' {_} R x := by simp
 
 @[simp]
 theorem toEmbedding_toHom (f : M ↪ₑ[L] N) : f.toEmbedding.toHom = f.toHom :=
@@ -281,7 +281,7 @@ namespace Equiv
 /-- A first-order equivalence is also an elementary embedding. -/
 def toElementaryEmbedding (f : M ≃[L] N) : M ↪ₑ[L] N where
   toFun := f
-  map_formula' n φ x := by aesop
+  map_formula' n φ x := by simp
 
 @[simp]
 theorem toElementaryEmbedding_toEmbedding (f : M ≃[L] N) :
diff --git a/Mathlib/ModelTheory/Substructures.lean b/Mathlib/ModelTheory/Substructures.lean
index 8b6541e29a94e..6ff42480b1d52 100644
--- a/Mathlib/ModelTheory/Substructures.lean
+++ b/Mathlib/ModelTheory/Substructures.lean
@@ -890,8 +890,8 @@ noncomputable def substructureEquivMap (f : M ↪[L] N) (s : L.Substructure M) :
             (codRestrict (s.map f.toHom) (f.domRestrict s) (fun ⟨m, hm⟩ => ⟨m, hm, rfl⟩)
                 ⟨m, hm⟩).2).2)
   right_inv := fun ⟨_, hn⟩ => Subtype.mk_eq_mk.2 (Classical.choose_spec hn).2
-  map_fun' {n} f x := by aesop
-  map_rel' {n} R x := by aesop
+  map_fun' {n} f x := by simp
+  map_rel' {n} R x := by simp
 
 @[simp]
 theorem substructureEquivMap_apply (f : M ↪[L] N) (p : L.Substructure M) (x : p) :
@@ -910,8 +910,8 @@ theorem subtype_substructureEquivMap (f : M ↪[L] N) (s : L.Substructure M) :
   left_inv m :=
     f.injective (Classical.choose_spec (codRestrict f.toHom.range f f.toHom.mem_range_self m).2)
   right_inv := fun ⟨_, hn⟩ => Subtype.mk_eq_mk.2 (Classical.choose_spec hn)
-  map_fun' {n} f x := by aesop
-  map_rel' {n} R x := by aesop
+  map_fun' {n} f x := by simp
+  map_rel' {n} R x := by simp
 
 @[simp]
 theorem equivRange_apply (f : M ↪[L] N) (x : M) : (f.equivRange x : N) = f x :=
diff --git a/Mathlib/Order/BooleanSubalgebra.lean b/Mathlib/Order/BooleanSubalgebra.lean
index 24751706b1099..4419c6cc58077 100644
--- a/Mathlib/Order/BooleanSubalgebra.lean
+++ b/Mathlib/Order/BooleanSubalgebra.lean
@@ -160,10 +160,10 @@ instance instTop : Top (BooleanSubalgebra α) where
 /-- The trivial boolean subalgebra of a lattice. -/
 instance instBot : Bot (BooleanSubalgebra α) where
   bot.carrier := {⊥, ⊤}
-  bot.bot_mem' := by aesop
-  bot.compl_mem' := by aesop
-  bot.supClosed' _ := by aesop
-  bot.infClosed' _ := by aesop
+  bot.bot_mem' := by simp
+  bot.compl_mem' := by simp
+  bot.supClosed' _ := by simp
+  bot.infClosed' _ := by simp
 
 /-- The inf of two boolean subalgebras is their intersection. -/
 instance instInf : Min (BooleanSubalgebra α) where
diff --git a/Mathlib/Order/Interval/Set/Basic.lean b/Mathlib/Order/Interval/Set/Basic.lean
index fb3aefe5d8181..06d3ef45f57c2 100644
--- a/Mathlib/Order/Interval/Set/Basic.lean
+++ b/Mathlib/Order/Interval/Set/Basic.lean
@@ -492,6 +492,54 @@ theorem not_mem_Ioo_of_le (ha : c ≤ a) : c ∉ Ioo a b := fun h => lt_irrefl _
 
 theorem not_mem_Ioo_of_ge (hb : b ≤ c) : c ∉ Ioo a b := fun h => lt_irrefl _ <| h.2.trans_le hb
 
+section matched_intervals
+
+@[simp] theorem Icc_eq_Ioc_same_iff : Icc a b = Ioc a b ↔ ¬a ≤ b where
+  mp h := by simpa using Set.ext_iff.mp h a
+  mpr h := by rw [Icc_eq_empty h, Ioc_eq_empty (mt le_of_lt h)]
+
+@[simp] theorem Icc_eq_Ico_same_iff : Icc a b = Ico a b ↔ ¬a ≤ b where
+  mp h := by simpa using Set.ext_iff.mp h b
+  mpr h := by rw [Icc_eq_empty h, Ico_eq_empty (mt le_of_lt h)]
+
+@[simp] theorem Icc_eq_Ioo_same_iff : Icc a b = Ioo a b ↔ ¬a ≤ b where
+  mp h := by simpa using Set.ext_iff.mp h b
+  mpr h := by rw [Icc_eq_empty h, Ioo_eq_empty (mt le_of_lt h)]
+
+@[simp] theorem Ioc_eq_Ico_same_iff : Ioc a b = Ico a b ↔ ¬a < b where
+  mp h := by simpa using Set.ext_iff.mp h a
+  mpr h := by rw [Ioc_eq_empty h, Ico_eq_empty h]
+
+@[simp] theorem Ioo_eq_Ioc_same_iff : Ioo a b = Ioc a b ↔ ¬a < b where
+  mp h := by simpa using Set.ext_iff.mp h b
+  mpr h := by rw [Ioo_eq_empty h, Ioc_eq_empty h]
+
+@[simp] theorem Ioo_eq_Ico_same_iff : Ioo a b = Ico a b ↔ ¬a < b where
+  mp h := by simpa using Set.ext_iff.mp h a
+  mpr h := by rw [Ioo_eq_empty h, Ico_eq_empty h]
+
+-- Mirrored versions of the above for `simp`.
+
+@[simp] theorem Ioc_eq_Icc_same_iff : Ioc a b = Icc a b ↔ ¬a ≤ b :=
+  eq_comm.trans Icc_eq_Ioc_same_iff
+
+@[simp] theorem Ico_eq_Icc_same_iff : Ico a b = Icc a b ↔ ¬a ≤ b :=
+  eq_comm.trans Icc_eq_Ico_same_iff
+
+@[simp] theorem Ioo_eq_Icc_same_iff : Ioo a b = Icc a b ↔ ¬a ≤ b :=
+  eq_comm.trans Icc_eq_Ioo_same_iff
+
+@[simp] theorem Ico_eq_Ioc_same_iff : Ico a b = Ioc a b ↔ ¬a < b :=
+  eq_comm.trans Ioc_eq_Ico_same_iff
+
+@[simp] theorem Ioc_eq_Ioo_same_iff : Ioc a b = Ioo a b ↔ ¬a < b :=
+  eq_comm.trans Ioo_eq_Ioc_same_iff
+
+@[simp] theorem Ico_eq_Ioo_same_iff : Ico a b = Ioo a b ↔ ¬a < b :=
+  eq_comm.trans Ioo_eq_Ico_same_iff
+
+end matched_intervals
+
 end Preorder
 
 section PartialOrder
@@ -1460,6 +1508,7 @@ theorem Ioc_union_Ioc_union_Ioc_cycle :
   all_goals
   solve_by_elim (config := { maxDepth := 5 }) [min_le_of_left_le, min_le_of_right_le,
        le_max_of_le_left, le_max_of_le_right, le_refl]
+
 end LinearOrder
 
 /-!
diff --git a/Mathlib/Order/SuccPred/Limit.lean b/Mathlib/Order/SuccPred/Limit.lean
index aa87d9363f44a..60eb29fc2d6f9 100644
--- a/Mathlib/Order/SuccPred/Limit.lean
+++ b/Mathlib/Order/SuccPred/Limit.lean
@@ -338,13 +338,21 @@ theorem isLUB_Iio_iff_isSuccPrelimit : IsLUB (Iio a) a ↔ IsSuccPrelimit a := b
   obtain rfl := isLUB_Iic.unique ha
   cases hb.lt.false
 
-lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hx : a ∉ s) :
+lemma _root_.IsLUB.isSuccPrelimit_of_not_mem {s : Set α} (hs : IsLUB s a) (ha : a ∉ s) :
     IsSuccPrelimit a := by
   intro b hb
   obtain ⟨c, hc, hbc, hca⟩ := hs.exists_between hb.lt
   obtain rfl := (hb.ge_of_gt hbc).antisymm hca
   contradiction
 
+lemma _root_.IsLUB.isSuccLimit_of_not_mem {s : Set α} (hs : IsLUB s a) (hs' : s.Nonempty)
+    (ha : a ∉ s) : IsSuccLimit a := by
+  refine ⟨?_, hs.isSuccPrelimit_of_not_mem ha⟩
+  obtain ⟨b, hb⟩ := hs'
+  obtain rfl | hb := (hs.1 hb).eq_or_lt
+  · contradiction
+  · exact hb.not_isMin
+
 variable [SuccOrder α]
 
 theorem IsSuccPrelimit.le_succ_iff (hb : IsSuccPrelimit b) : b ≤ succ a ↔ b ≤ a :=
@@ -650,9 +658,13 @@ theorem IsPredLimit.isGLB_Ioi (ha : IsPredLimit a) : IsGLB (Ioi a) a :=
 theorem isGLB_Ioi_iff_isPredPrelimit : IsGLB (Ioi a) a ↔ IsPredPrelimit a := by
   simpa using isLUB_Iio_iff_isSuccPrelimit (a := toDual a)
 
-lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hx : a ∉ s) :
+lemma _root_.IsGLB.isPredPrelimit_of_not_mem {s : Set α} (hs : IsGLB s a) (ha : a ∉ s) :
     IsPredPrelimit a := by
-  simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem hx
+  simpa using (IsGLB.dual hs).isSuccPrelimit_of_not_mem ha
+
+lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
+    (ha : a ∉ s) : IsPredLimit a := by
+  simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha
 
 variable [PredOrder α]
 
diff --git a/Mathlib/Probability/Kernel/Disintegration/Basic.lean b/Mathlib/Probability/Kernel/Disintegration/Basic.lean
index 8d443a75e791c..aeae2b78f63d7 100644
--- a/Mathlib/Probability/Kernel/Disintegration/Basic.lean
+++ b/Mathlib/Probability/Kernel/Disintegration/Basic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2024 Yaël Dillies, Kin Yau James Wong. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Kin Yau James Wong, Rémy Degenne
 -/
+import Mathlib.MeasureTheory.Function.AEEqOfLIntegral
 import Mathlib.Probability.Kernel.Composition.MeasureCompProd
 
 /-!
@@ -126,9 +127,62 @@ class IsCondKernel : Prop where
 instance instIsCondKernel_zero (κCond : Kernel (α × β) Ω) : IsCondKernel 0 κCond where
   disintegrate := by simp
 
-variable [κ.IsCondKernel κCond]
+lemma disintegrate [κ.IsCondKernel κCond] : κ.fst ⊗ₖ κCond = κ := IsCondKernel.disintegrate
+
+/-- A conditional kernel is almost everywhere a probability measure. -/
+lemma IsCondKernel.isProbabilityMeasure_ae [IsFiniteKernel κ.fst] [κ.IsCondKernel κCond] (a : α) :
+    ∀ᵐ b ∂(κ.fst a), IsProbabilityMeasure (κCond (a, b)) := by
+  have h := disintegrate κ κCond
+  by_cases h_sfin : IsSFiniteKernel κCond
+  swap; · rw [Kernel.compProd_of_not_isSFiniteKernel_right _ _ h_sfin] at h; simp [h.symm]
+  suffices ∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ = 1 by
+    convert this with b
+    exact ⟨fun _ ↦ measure_univ, fun h ↦ ⟨h⟩⟩
+  suffices (∀ᵐ b ∂(κ.fst a), κCond (a, b) Set.univ ≤ 1)
+      ∧ (∀ᵐ b ∂(κ.fst a), 1 ≤ κCond (a, b) Set.univ) by
+    filter_upwards [this.1, this.2] with b h1 h2 using le_antisymm h1 h2
+  have h_eq s (hs : MeasurableSet s) :
+      ∫⁻ b, s.indicator (fun b ↦ κCond (a, b) Set.univ) b ∂κ.fst a = κ.fst a s := by
+    conv_rhs => rw [← h]
+    rw [fst_compProd_apply _ _ _ hs]
+  have h_meas : Measurable fun b ↦ κCond (a, b) Set.univ :=
+    (κCond.measurable_coe MeasurableSet.univ).comp measurable_prod_mk_left
+  constructor
+  · rw [ae_le_const_iff_forall_gt_measure_zero]
+    intro r hr
+    let s := {b | r ≤ κCond (a, b) Set.univ}
+    have hs : MeasurableSet s := h_meas measurableSet_Ici
+    have h_2_le : s.indicator (fun _ ↦ r) ≤ s.indicator (fun b ↦ (κCond (a, b)) Set.univ) := by
+      intro b
+      by_cases hbs : b ∈ s
+      · simpa [hbs]
+      · simp [hbs]
+    have : ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) ≤ κ.fst a s :=
+      (lintegral_mono h_2_le).trans_eq (h_eq s hs)
+    rw [lintegral_indicator_const hs] at this
+    by_contra h_ne_zero
+    rw [← not_lt] at this
+    refine this ?_
+    conv_lhs => rw [← one_mul (κ.fst a s)]
+    exact ENNReal.mul_lt_mul_right' h_ne_zero (measure_ne_top _ _) hr
+  · rw [ae_const_le_iff_forall_lt_measure_zero]
+    intro r hr
+    let s := {b | κCond (a, b) Set.univ ≤ r}
+    have hs : MeasurableSet s := h_meas measurableSet_Iic
+    have h_2_le : s.indicator (fun b ↦ (κCond (a, b)) Set.univ) ≤ s.indicator (fun _ ↦ r) := by
+      intro b
+      by_cases hbs : b ∈ s
+      · simpa [hbs]
+      · simp [hbs]
+    have : κ.fst a s ≤ ∫⁻ b, s.indicator (fun _ ↦ r) b ∂(κ.fst a) :=
+      (h_eq s hs).symm.trans_le (lintegral_mono h_2_le)
+    rw [lintegral_indicator_const hs] at this
+    by_contra h_ne_zero
+    rw [← not_lt] at this
+    refine this ?_
+    conv_rhs => rw [← one_mul (κ.fst a s)]
+    exact ENNReal.mul_lt_mul_right' h_ne_zero (measure_ne_top _ _) hr
 
-lemma disintegrate : κ.fst ⊗ₖ κCond = κ := IsCondKernel.disintegrate
 
 /-! #### Existence of a disintegrating kernel in a countable space -/
 
diff --git a/Mathlib/Probability/StrongLaw.lean b/Mathlib/Probability/StrongLaw.lean
index 734ac6c8622b2..af74169d09b3b 100644
--- a/Mathlib/Probability/StrongLaw.lean
+++ b/Mathlib/Probability/StrongLaw.lean
@@ -426,7 +426,7 @@ theorem strong_law_aux1 {c : ℝ} (c_one : 1 < c) {ε : ℝ} (εpos : 0 < ε) :
         · simp only [mem_sigma, mem_range, filter_congr_decidable, mem_filter, and_imp,
             Sigma.forall]
           exact fun a b haN hb ↦ ⟨hb.trans_le <| u_mono <| Nat.le_pred_of_lt haN, haN, hb⟩
-        all_goals aesop
+        all_goals simp
       _ ≤ ∑ j ∈ range (u (N - 1)), c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j] := by
         apply sum_le_sum fun j hj => ?_
         rcases @eq_zero_or_pos _ _ j with (rfl | hj)
diff --git a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
index ff50887857737..1c8844cd09b48 100644
--- a/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
+++ b/Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
@@ -797,7 +797,7 @@ def shortComplexH1Iso : (inhomogeneousCochains A).sc' 0 1 2 ≅ shortComplexH1 A
 /-- The 1-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
 `oneCocycles A`, which is a simpler type. -/
 def isoOneCocycles : cocycles A 1 ≅ ModuleCat.of k (oneCocycles A) :=
-  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by simp) (by simp) ≪≫
     cyclesMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatCyclesIso
 
 lemma isoOneCocycles_hom_comp_subtype :
@@ -817,7 +817,7 @@ lemma toCocycles_comp_isoOneCocycles_hom :
 /-- The 1st group cohomology of `A`, defined as the 1st cohomology of the complex of inhomogeneous
 cochains, is isomorphic to `oneCocycles A ⧸ oneCoboundaries A`, which is a simpler type. -/
 def isoH1 : groupCohomology A 1 ≅ ModuleCat.of k (H1 A) :=
-  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by simp) (by simp) ≪≫
     homologyMapIso (shortComplexH1Iso A) ≪≫ (shortComplexH1 A).moduleCatHomologyIso
 
 lemma groupCohomologyπ_comp_isoH1_hom  :
@@ -846,7 +846,7 @@ def shortComplexH2Iso :
 /-- The 2-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
 `twoCocycles A`, which is a simpler type. -/
 def isoTwoCocycles : cocycles A 2 ≅ ModuleCat.of k (twoCocycles A) :=
-  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+  (inhomogeneousCochains A).cyclesIsoSc' _ _ _ (by simp) (by simp) ≪≫
     cyclesMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatCyclesIso
 
 lemma isoTwoCocycles_hom_comp_subtype :
@@ -866,7 +866,7 @@ lemma toCocycles_comp_isoTwoCocycles_hom :
 /-- The 2nd group cohomology of `A`, defined as the 2nd cohomology of the complex of inhomogeneous
 cochains, is isomorphic to `twoCocycles A ⧸ twoCoboundaries A`, which is a simpler type. -/
 def isoH2 : groupCohomology A 2 ≅ ModuleCat.of k (H2 A) :=
-  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by aesop) (by aesop) ≪≫
+  (inhomogeneousCochains A).homologyIsoSc' _ _ _ (by simp) (by simp) ≪≫
     homologyMapIso (shortComplexH2Iso A) ≪≫ (shortComplexH2 A).moduleCatHomologyIso
 
 lemma groupCohomologyπ_comp_isoH2_hom  :
diff --git a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
index 4ac8d7b974ccc..80039d291af17 100644
--- a/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
+++ b/Mathlib/RingTheory/AdicCompletion/Functoriality.lean
@@ -128,7 +128,7 @@ private theorem adicCompletionAux_val_apply (f : M →ₗ[R] N) {n : ℕ} (x : A
 def map (f : M →ₗ[R] N) :
     AdicCompletion I M →ₗ[AdicCompletion I R] AdicCompletion I N where
   toFun := adicCompletionAux I f
-  map_add' := by aesop
+  map_add' := by simp
   map_smul' r x := by
     ext n
     simp only [adicCompletionAux_val_apply, smul_eval, smul_eq_mul, RingHom.id_apply]
diff --git a/Mathlib/RingTheory/MvPolynomial/Localization.lean b/Mathlib/RingTheory/MvPolynomial/Localization.lean
index 2a8977ca29026..e3fb28794c4d7 100644
--- a/Mathlib/RingTheory/MvPolynomial/Localization.lean
+++ b/Mathlib/RingTheory/MvPolynomial/Localization.lean
@@ -3,11 +3,13 @@ Copyright (c) 2024 Christian Merten. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Christian Merten
 -/
+import Mathlib.Algebra.Module.LocalizedModule.IsLocalization
 import Mathlib.Algebra.MvPolynomial.CommRing
 import Mathlib.RingTheory.Ideal.Quotient.Operations
 import Mathlib.RingTheory.Localization.Away.Basic
-import Mathlib.RingTheory.Localization.Basic
+import Mathlib.RingTheory.Localization.BaseChange
 import Mathlib.RingTheory.MvPolynomial.Basic
+import Mathlib.RingTheory.TensorProduct.MvPolynomial
 
 /-!
 
@@ -36,40 +38,9 @@ attribute [local instance] algebraMvPolynomial
 If `S` is the localization of `R` at a submonoid `M`, then `MvPolynomial σ S`
 is the localization of `MvPolynomial σ R` at `M.map MvPolynomial.C`.
 -/
-instance isLocalization : IsLocalization (M.map <| C (σ := σ))
-    (MvPolynomial σ S) where
-  map_units' := by
-    rintro ⟨p, q, hq, rfl⟩
-    simp only [algebraMap_def, map_C]
-    exact IsUnit.map _ (IsLocalization.map_units _ ⟨q, hq⟩)
-  surj' p := by
-    simp only [algebraMap_def, Prod.exists, Subtype.exists,
-      Submonoid.mem_map, exists_prop, exists_exists_and_eq_and, map_C]
-    refine induction_on' p ?_ ?_
-    · intro u s
-      obtain ⟨⟨r, m⟩, hr⟩ := IsLocalization.surj M s
-      use monomial u r, m, m.property
-      simp only [map_monomial]
-      rw [← hr, mul_comm, C_mul_monomial, mul_comm]
-    · intro p p' ⟨x, m, hm, hxm⟩ ⟨x', m', hm', hxm'⟩
-      use x * (C m') + x' * (C m), m * m', Submonoid.mul_mem _ hm hm'
-      simp only [map_mul, map_add, map_C]
-      rw [add_mul, ← mul_assoc, hxm, ← mul_assoc, ← hxm, ← hxm']
-      ring
-  exists_of_eq {p q} := by
-    intro h
-    simp_rw [algebraMap_def, MvPolynomial.ext_iff, coeff_map] at h
-    choose c hc using (fun m ↦ IsLocalization.exists_of_eq (M := M) (h m))
-    simp only [Subtype.exists, Submonoid.mem_map, exists_prop, exists_exists_and_eq_and]
-    classical
-    refine ⟨Finset.prod (p.support ∪ q.support) (fun m ↦ c m), ?_, ?_⟩
-    · exact M.prod_mem (fun m _ ↦ (c m).property)
-    · ext m
-      simp only [coeff_C_mul]
-      by_cases h : m ∈ p.support ∪ q.support
-      · exact Finset.prod_mul_eq_prod_mul_of_exists m h (hc m)
-      · simp only [Finset.mem_union, mem_support_iff, ne_eq, not_or, Decidable.not_not] at h
-        rw [h.left, h.right]
+instance isLocalization : IsLocalization (M.map <| C (σ := σ)) (MvPolynomial σ S) :=
+  isLocalizedModule_iff_isLocalization.mp <| (isLocalizedModule_iff_isBaseChange M S _).mpr <|
+    .of_equiv (algebraTensorAlgEquiv _ _).toLinearEquiv fun _ ↦ by simp
 
 lemma isLocalization_C_mk' (a : R) (m : M) :
     C (IsLocalization.mk' S a m) = IsLocalization.mk' (MvPolynomial σ S) (C (σ := σ) a)
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index ee879a0ea1dde..c914bbd405ef9 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -338,7 +338,7 @@ theorem enum_succ_eq_top {o : Ordinal} :
 theorem has_succ_of_type_succ_lt {α} {r : α → α → Prop} [wo : IsWellOrder α r]
     (h : ∀ a < type r, succ a < type r) (x : α) : ∃ y, r x y := by
   use enum r ⟨succ (typein r x), h _ (typein_lt_type r x)⟩
-  convert enum_lt_enum (o₁ := ⟨_, typein_lt_type r x⟩) (o₂ := ⟨_, h _ (typein_lt_type r x)⟩).mpr _
+  convert enum_lt_enum.mpr _
   · rw [enum_typein]
   · rw [Subtype.mk_lt_mk, lt_succ_iff]
 
@@ -364,12 +364,6 @@ theorem typein_ordinal (o : Ordinal.{u}) :
   rintro ⟨α, r, wo⟩; apply Quotient.sound
   constructor; refine ((RelIso.preimage Equiv.ulift r).trans (enum r).symm).symm
 
--- Porting note: `· < ·` requires a type ascription for an `IsWellOrder` instance.
-@[deprecated typein_ordinal (since := "2024-09-19")]
-theorem type_subrel_lt (o : Ordinal.{u}) :
-    type (@Subrel Ordinal (· < ·) { o' : Ordinal | o' < o }) = Ordinal.lift.{u + 1} o :=
-  typein_ordinal o
-
 theorem mk_Iio_ordinal (o : Ordinal.{u}) :
     #(Iio o) = Cardinal.lift.{u + 1} o.card := by
   rw [lift_card, ← typein_ordinal]
diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
index a663b8dadc323..33a1d3e36a834 100644
--- a/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -487,10 +487,8 @@ theorem typein_surjOn (r : α → α → Prop) [IsWellOrder α r] :
 
 That is, `enum` maps an initial segment of the ordinals, those less than the order type of `r`, to
 the elements of `α`. -/
--- The explicit typing is required in order for `simp` to work properly.
 @[simps! symm_apply_coe]
-def enum (r : α → α → Prop) [IsWellOrder α r] :
-    @RelIso { o // o < type r } α (Subrel (· < ·) { o | o < type r }) r :=
+def enum (r : α → α → Prop) [IsWellOrder α r] : (· < · : Iio (type r) → Iio (type r) → Prop) ≃r r :=
   (typein r).subrelIso
 
 @[simp]
@@ -507,20 +505,20 @@ theorem enum_typein (r : α → α → Prop) [IsWellOrder α r] (a : α) :
     enum r ⟨typein r a, typein_lt_type r a⟩ = a :=
   enum_type (PrincipalSeg.ofElement r a)
 
-theorem enum_lt_enum {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : {o // o < type r}} :
+theorem enum_lt_enum {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
     r (enum r o₁) (enum r o₂) ↔ o₁ < o₂ :=
   (enum _).map_rel_iff
 
-theorem enum_le_enum (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : {o // o < type r}} :
+theorem enum_le_enum (r : α → α → Prop) [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
     ¬r (enum r o₁) (enum r o₂) ↔ o₂ ≤ o₁ := by
   rw [enum_lt_enum (r := r), not_lt]
 
 @[simp]
-theorem enum_le_enum' (a : Ordinal) {o₁ o₂ : {o // o < type (· < ·)}} :
+theorem enum_le_enum' (a : Ordinal) {o₁ o₂ : Iio (type (· < ·))} :
     enum (· < ·) o₁ ≤ enum (α := a.toType) (· < ·) o₂ ↔ o₁ ≤ o₂ := by
   rw [← enum_le_enum, not_lt]
 
-theorem enum_inj {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : {o // o < type r}} :
+theorem enum_inj {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : Iio (type r)} :
     enum r o₁ = enum r o₂ ↔ o₁ = o₂ :=
   EmbeddingLike.apply_eq_iff_eq _
 
diff --git a/Mathlib/Topology/Category/Profinite/AsLimit.lean b/Mathlib/Topology/Category/Profinite/AsLimit.lean
index 72fb66b943303..a417cb6fdd284 100644
--- a/Mathlib/Topology/Category/Profinite/AsLimit.lean
+++ b/Mathlib/Topology/Category/Profinite/AsLimit.lean
@@ -45,7 +45,7 @@ def fintypeDiagram : DiscreteQuotient X ⥤ FintypeCat where
   map f := DiscreteQuotient.ofLE f.le
   -- Porting note: `map_comp` used to be proved by default by `aesop_cat`.
   -- once `aesop_cat` can prove this again, remove the entire `map_comp` here.
-  map_comp _ _ := by ext; aesop_cat
+  map_comp _ _ := by ext; simp
 
 /-- An abbreviation for `X.fintypeDiagram ⋙ FintypeCat.toProfinite`. -/
 abbrev diagram : DiscreteQuotient X ⥤ Profinite :=
diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean
index 745a728ee1127..9147bdcc6b1f6 100644
--- a/Mathlib/Topology/ContinuousOn.lean
+++ b/Mathlib/Topology/ContinuousOn.lean
@@ -215,7 +215,7 @@ theorem union_mem_nhds_of_mem_nhdsWithin {b : α}
     {L : Set α} (hL : L ∈ nhdsWithin b I₁)
     {R : Set α} (hR : R ∈ nhdsWithin b I₂) : L ∪ R ∈ nhds b := by
   rw [← nhdsWithin_univ b, h, nhdsWithin_union]
-  exact ⟨mem_of_superset hL (by aesop), mem_of_superset hR (by aesop)⟩
+  exact ⟨mem_of_superset hL (by simp), mem_of_superset hR (by simp)⟩
 
 
 /-- Writing a punctured neighborhood filter as a sup of left and right filters. -/
diff --git a/Mathlib/Topology/Order/Compact.lean b/Mathlib/Topology/Order/Compact.lean
index 865a0c4150338..041ed9ae203b1 100644
--- a/Mathlib/Topology/Order/Compact.lean
+++ b/Mathlib/Topology/Order/Compact.lean
@@ -155,6 +155,26 @@ instance compactSpace_Icc (a b : α) : CompactSpace (Icc a b) :=
 
 end
 
+section openIntervals
+variable {α : Type*} [LinearOrder α] [TopologicalSpace α] [OrderTopology α] [DenselyOrdered α]
+
+/-- `Set.Ico a b` is only compact if it is empty. -/
+@[simp]
+theorem isCompact_Ico_iff {a b : α} : IsCompact (Set.Ico a b) ↔ b ≤ a :=
+  ⟨fun h => isClosed_Ico_iff.mp h.isClosed, by simp_all⟩
+
+/-- `Set.Ioc a b` is only compact if it is empty. -/
+@[simp]
+theorem isCompact_Ioc_iff {a b : α} : IsCompact (Set.Ioc a b) ↔ b ≤ a :=
+  ⟨fun h => isClosed_Ioc_iff.mp h.isClosed, by simp_all⟩
+
+/-- `Set.Ioo a b` is only compact if it is empty. -/
+@[simp]
+theorem isCompact_Ioo_iff {a b : α} : IsCompact (Set.Ioo a b) ↔ b ≤ a :=
+  ⟨fun h => isClosed_Ioo_iff.mp h.isClosed, by simp_all⟩
+
+end openIntervals
+
 /-!
 ### Extreme value theorem
 -/
diff --git a/Mathlib/Topology/Order/DenselyOrdered.lean b/Mathlib/Topology/Order/DenselyOrdered.lean
index f7a40b1ae2311..0c981229bfc16 100644
--- a/Mathlib/Topology/Order/DenselyOrdered.lean
+++ b/Mathlib/Topology/Order/DenselyOrdered.lean
@@ -374,8 +374,7 @@ theorem Dense.exists_countable_dense_subset_no_bot_top [Nontrivial α] {s : Set
   · simp [hx]
   · simp [hx]
 
-variable (α)
-
+variable (α) in
 /-- If `α` is a nontrivial separable dense linear order, then there exists a
 countable dense set `s : Set α` that contains neither top nor bottom elements of `α`.
 For a dense set containing both bot and top elements, see
@@ -384,4 +383,28 @@ theorem exists_countable_dense_no_bot_top [SeparableSpace α] [Nontrivial α] :
     ∃ s : Set α, s.Countable ∧ Dense s ∧ (∀ x, IsBot x → x ∉ s) ∧ ∀ x, IsTop x → x ∉ s := by
   simpa using dense_univ.exists_countable_dense_subset_no_bot_top
 
+/-- `Set.Ico a b` is only closed if it is empty. -/
+@[simp]
+theorem isClosed_Ico_iff {a b : α} : IsClosed (Set.Ico a b) ↔ b ≤ a := by
+  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
+  have := h.closure_eq
+  rw [closure_Ico hab.ne, Icc_eq_Ico_same_iff] at this
+  exact this hab.le
+
+/-- `Set.Ioc a b` is only closed if it is empty. -/
+@[simp]
+theorem isClosed_Ioc_iff {a b : α} : IsClosed (Set.Ioc a b) ↔ b ≤ a := by
+  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
+  have := h.closure_eq
+  rw [closure_Ioc hab.ne, Icc_eq_Ioc_same_iff] at this
+  exact this hab.le
+
+/-- `Set.Ioo a b` is only closed if it is empty. -/
+@[simp]
+theorem isClosed_Ioo_iff {a b : α} : IsClosed (Set.Ioo a b) ↔ b ≤ a := by
+  refine ⟨fun h => le_of_not_lt fun hab => ?_, by simp_all⟩
+  have := h.closure_eq
+  rw [closure_Ioo hab.ne, Icc_eq_Ioo_same_iff] at this
+  exact this hab.le
+
 end DenselyOrdered
diff --git a/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean b/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
index 318e4ad961054..d316325a6727d 100644
--- a/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
+++ b/Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean
@@ -154,7 +154,7 @@ def generateEquivalenceOpensLe (hY : Y = iSup U) :
   inverse := generateEquivalenceOpensLe_inverse' _ hY
   unitIso := eqToIso <| CategoryTheory.Functor.ext
     (by rintro ⟨⟨_, _⟩, _⟩; dsimp; congr)
-    (by intros; refine Over.OverMorphism.ext ?_; aesop_cat)
+    (by intros; refine Over.OverMorphism.ext ?_; simp)
   counitIso := eqToIso <| CategoryTheory.Functor.hext
     (by intro; refine FullSubcategory.ext ?_; rfl) (by intros; rfl)
 
diff --git a/docs/1000.yaml b/docs/1000.yaml
index 64168a6a6f4ae..50d0e3fb4af8f 100644
--- a/docs/1000.yaml
+++ b/docs/1000.yaml
@@ -1329,7 +1329,7 @@ Q1191862:
 Q1194053:
   title: Metrization theorems
   decl: TopologicalSpace.metrizableSpace_of_t3_secondCountable
-  comment: "Urysohn's metrization theorem (only)"
+  # comment: "Urysohn's metrization theorem (only)"
 
 Q1196538:
   title: Descartes's theorem
@@ -1384,7 +1384,7 @@ Q1306092:
 Q1306095:
   title: Whitney embedding theorem
   decl: exists_embedding_euclidean_of_compact
-  comment: "baby version: for compact manifolds; embedding into some *n*"
+  # comment: "baby version: for compact manifolds; embedding into some *n*"
 
 Q1307676:
   title: Künneth theorem
diff --git a/lake-manifest.json b/lake-manifest.json
index 8a7f0e3ba49a2..795e5c8c6acca 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8ce422eb59adf557fac184f8b1678c75fa03075c",
+   "rev": "b2e8b6868397fcd93c00aca7278b933c16c0ffb3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "v4.16.0-rc1",