merge master

Author: kim-em

Mathlib/Algebra/Category/Grp/LeftExactFunctor.lean

@@ -77,15 +77,15 @@ noncomputable def unitIsoAux (F : C ⥤ AddCommGrp.{v}) [PreservesFiniteLimits F
   letI : F.Monoidal := .ofChosenFiniteProducts _
   refine CommGrp_.mkIso Multiplicative.toAdd.toIso (by
     erw [Functor.mapCommGrp_obj_grp_one]
-    aesop_cat) ?_
+    cat_disch) ?_
   dsimp [-Functor.comp_map, -ConcreteCategory.forget_map_eq_coe, -forget_map]
   have : F.Additive := Functor.additive_of_preserves_binary_products _
   simp only [Category.id_comp]
   erw [Functor.mapCommGrp_obj_grp_mul]
   erw [Functor.comp_map, F.map_add, Functor.Monoidal.μ_comp F (forget AddCommGrp) X X,
     Category.assoc, ← Functor.map_comp, Preadditive.comp_add, Functor.Monoidal.μ_fst,
     Functor.Monoidal.μ_snd]
-  aesop_cat
+  cat_disch
 
 /-- Implementation, see `leftExactFunctorForgetEquivalence`. -/
 noncomputable def unitIso : 𝟭 (C ⥤ₗ AddCommGrp) ≅

Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

@@ -77,7 +77,7 @@ instance symmetricCategory : SymmetricCategory (ModuleCat.{u} R) where
   symmetry _ _ := by
     ext : 1
     apply TensorProduct.ext'
-    aesop_cat
+    cat_disch
 
 @[simp]
 theorem braiding_hom_apply {M N : ModuleCat.{u} R} (m : M) (n : N) :

Mathlib/Algebra/Category/ModuleCat/Presheaf.lean

@@ -44,7 +44,7 @@ structure PresheafOfModules where
   map_id (X : Cᵒᵖ) :
     map (𝟙 X) = (ModuleCat.restrictScalarsId' (R.map (𝟙 X)).hom
       (congrArg RingCat.Hom.hom (R.map_id X))).inv.app _ := by
-        aesop_cat
+        cat_disch
   map_comp {X Y Z : Cᵒᵖ} (f : X ⟶ Y) (g : Y ⟶ Z) :
     map (f ≫ g) = map f ≫ (ModuleCat.restrictScalars _).map (map g) ≫
       (ModuleCat.restrictScalarsComp' (R.map f).hom (R.map g).hom (R.map (f ≫ g)).hom

Mathlib/Algebra/Homology/Additive.lean

@@ -167,7 +167,7 @@ theorem NatTrans.mapHomologicalComplex_comp (c : ComplexShape ι) {F G H : W₁
     (α : F ⟶ G) (β : G ⟶ H) :
     NatTrans.mapHomologicalComplex (α ≫ β) c =
       NatTrans.mapHomologicalComplex α c ≫ NatTrans.mapHomologicalComplex β c := by
-  aesop_cat
+  cat_disch
 
 @[reassoc]
 theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : W₁ ⥤ W₂}

Mathlib/Algebra/Homology/CommSq.lean

@@ -60,7 +60,7 @@ noncomputable def CommSq.isColimitEquivIsColimitCokernelCofork (sq : CommSq f g
       (fun s ↦ PushoutCocone.IsColimit.desc h
         (biprod.inl ≫ s.π) (biprod.inr ≫ s.π) (by
           rw [← sub_eq_zero, ← assoc, ← assoc, ← Preadditive.sub_comp]
-          convert s.condition <;> aesop_cat))
+          convert s.condition <;> cat_disch))
       (fun s ↦ by
         dsimp
         ext
@@ -96,7 +96,7 @@ noncomputable def CommSq.isColimitEquivIsColimitCokernelCofork (sq : CommSq f g
         apply Cofork.IsColimit.hom_ext h
         convert (h.fac (CokernelCofork.ofπ (biprod.desc s.inl s.inr)
           (by simp [s.condition])) .one).symm
-        aesop_cat)
+        cat_disch)
   left_inv _ := Subsingleton.elim _ _
   right_inv _ := Subsingleton.elim _ _
 
@@ -139,7 +139,7 @@ noncomputable def CommSq.isLimitEquivIsLimitKernelFork (sq : CommSq fst snd f g)
       (fun s ↦ PullbackCone.IsLimit.lift h
         (s.ι ≫ biprod.fst) (s.ι ≫ biprod.snd) (by
           rw [← sub_eq_zero, assoc, assoc, ← Preadditive.comp_sub]
-          convert s.condition <;> aesop_cat))
+          convert s.condition <;> cat_disch))
       (fun s ↦ by
         dsimp
         ext
@@ -173,7 +173,7 @@ noncomputable def CommSq.isLimitEquivIsLimitKernelFork (sq : CommSq fst snd f g)
         apply Fork.IsLimit.hom_ext h
         convert (h.fac (KernelFork.ofι (biprod.lift s.fst s.snd)
           (by simp [s.condition])) .zero).symm
-        aesop_cat)
+        cat_disch)
   left_inv _ := Subsingleton.elim _ _
   right_inv _ := Subsingleton.elim _ _
 

Mathlib/Algebra/Homology/DerivedCategory/SingleTriangle.lean

@@ -62,8 +62,8 @@ noncomputable def singleTriangleIso :
       triangleOfSES (hS.map_of_exact (HomologicalComplex.single C (ComplexShape.up ℤ) 0)) := by
   let e := (SingleFunctors.evaluation _ _ 0).mapIso (singleFunctorsPostcompQIso C)
   refine Triangle.isoMk _ _ (e.app S.X₁) (e.app S.X₂) (e.app S.X₃) ?_ ?_ ?_
-  · aesop_cat
-  · aesop_cat
+  · cat_disch
+  · cat_disch
   · dsimp [singleδ, e]
     rw [Category.assoc, Category.assoc, ← Functor.map_comp, SingleFunctors.inv_hom_id_hom_app]
     erw [Functor.map_id]

Mathlib/Algebra/Homology/ExactSequence.lean

@@ -56,13 +56,13 @@ theorem ShortComplex.mapToComposableArrows_app_2 {S₁ S₂ : ShortComplex C} (
 @[simp]
 theorem ShortComplex.mapToComposableArrows_id {S₁ : ShortComplex C} :
     (ShortComplex.mapToComposableArrows (𝟙 S₁)) = 𝟙 S₁.toComposableArrows := by
-  aesop_cat
+  cat_disch
 
 @[simp]
 theorem ShortComplex.mapToComposableArrows_comp {S₁ S₂ S₃ : ShortComplex C} (φ : S₁ ⟶ S₂)
     (ψ : S₂ ⟶ S₃) : ShortComplex.mapToComposableArrows (φ ≫ ψ) =
       ShortComplex.mapToComposableArrows φ ≫ ShortComplex.mapToComposableArrows ψ := by
-  aesop_cat
+  cat_disch
 
 namespace ComposableArrows
 

Mathlib/Algebra/Homology/HomotopyCofiber.lean

@@ -361,7 +361,7 @@ noncomputable def descEquiv (K : HomologicalComplex C c) (hc : ∀ j, ∃ i, c.R
   right_inv f := (eq_desc φ f hc).symm
   left_inv := fun ⟨α, hα⟩ => by
     rw [descSigma_ext_iff]
-    aesop_cat
+    cat_disch
 
 end homotopyCofiber
 

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

@@ -996,7 +996,7 @@ noncomputable def leftHomologyIsCokernel :
 lemma liftCycles_comp_cyclesMap (φ : S ⟶ S₁) [S₁.HasLeftHomology] :
     S.liftCycles k hk ≫ cyclesMap φ =
       S₁.liftCycles (k ≫ φ.τ₂) (by rw [assoc, φ.comm₂₃, reassoc_of% hk, zero_comp]) := by
-  aesop_cat
+  cat_disch
 
 variable {S}
 

Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

@@ -492,7 +492,7 @@ noncomputable def functorP : SnakeInput C ⥤ C where
   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]; simp
-  map_comp _ _ := by dsimp [P]; aesop_cat
+  map_comp _ _ := by dsimp [P]; cat_disch
 
 @[reassoc]
 lemma naturality_φ₂ (f : S₁ ⟶ S₂) : S₁.φ₂ ≫ f.f₂.τ₂ = functorP.map f ≫ S₂.φ₂ := by