Skip to content

Commit 95cdc7a

Browse files
kim-emkim-em
committed
chore: replace aesop with simp where possible (#20483)
I'm investigating how `aesop` is being used (and making comparisons with the in development `grind` tactic), but finding many uses of `aesop` can in fact just be replaced by `simp`. Hopefully using the simpler tool is both faster, and more readable. We'll see.
1 parent a57f317 commit 95cdc7a

123 files changed

Lines changed: 267 additions & 270 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

β€ŽMathlib/Algebra/Category/ModuleCat/Presheaf/Sheafify.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -318,7 +318,7 @@ noncomputable def sheafify : SheafOfModules.{v} R where
318318
def toSheafify : Mβ‚€ ⟢ (restrictScalars Ξ±).obj (sheafify Ξ± Ο†).val :=
319319
homMk Ο† (fun X rβ‚€ mβ‚€ ↦ by
320320
simpa using (Sheafify.map_smul_eq Ξ± Ο† (Ξ±.app _ rβ‚€) (Ο†.app _ mβ‚€) (πŸ™ _)
321-
rβ‚€ (by aesop) mβ‚€ (by simp)).symm)
321+
rβ‚€ (by simp) mβ‚€ (by simp)).symm)
322322

323323
lemma toSheafify_app_apply (X : Cα΅’α΅–) (x : Mβ‚€.obj X) :
324324
((toSheafify Ξ± Ο†).app X).hom x = Ο†.app X x := rfl

β€ŽMathlib/Algebra/Category/ModuleCat/Subobject.leanβ€Ž

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -85,8 +85,7 @@ theorem toKernelSubobject_arrow {M N : ModuleCat R} {f : M ⟢ N} (x : LinearMap
8585
suffices ((arrow ((kernelSubobject f))) ∘ (kernelSubobjectIso f β‰ͺ≫ kernelIsoKer f).inv) x = x by
8686
convert this
8787
rw [Iso.trans_inv, ← LinearMap.coe_comp, ← hom_comp, Category.assoc]
88-
simp only [Category.assoc, kernelSubobject_arrow', kernelIsoKer_inv_kernel_ΞΉ]
89-
aesop_cat
88+
simp
9089

9190
/-- An extensionality lemma showing that two elements of a cokernel by an image
9291
are equal if they differ by an element of the image.

β€ŽMathlib/Algebra/Category/Semigrp/Basic.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -44,7 +44,7 @@ namespace MagmaCat
4444
@[to_additive]
4545
instance bundledHom : BundledHom @MulHom :=
4646
⟨@MulHom.toFun, @MulHom.id, @MulHom.comp,
47-
by intros; apply @DFunLike.coe_injective, by aesop_cat, by aesop_cat⟩
47+
by intros; apply @DFunLike.coe_injective, by aesop_cat, by simp⟩
4848

4949
-- Porting note: deriving failed for `ConcreteCategory`,
5050
-- "default handlers have not been implemented yet"

β€ŽMathlib/Algebra/Homology/Additive.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ΞΉ} {F G : W
176176
(Ξ± : F ⟢ G) {C D : HomologicalComplex W₁ c} (f : C ⟢ D) :
177177
(F.mapHomologicalComplex c).map f ≫ (NatTrans.mapHomologicalComplex Ξ± c).app D =
178178
(NatTrans.mapHomologicalComplex Ξ± c).app C ≫ (G.mapHomologicalComplex c).map f := by
179-
aesop_cat
179+
simp
180180

181181
/-- A natural isomorphism between functors induces a natural isomorphism
182182
between those functors applied to homological complexes.

β€ŽMathlib/Algebra/Homology/Augment.leanβ€Ž

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ The components of this chain map are `C.d 1 0` in degree 0, and zero otherwise.
3737
-/
3838
def truncateTo [HasZeroObject V] [HasZeroMorphisms V] (C : ChainComplex V β„•) :
3939
truncate.obj C ⟢ (singleβ‚€ V).obj (C.X 0) :=
40-
(toSingleβ‚€Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 1 0, by aesop⟩
40+
(toSingleβ‚€Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 1 0, by simp⟩
4141

4242
-- PROJECT when `V` is abelian (but not generally?)
4343
-- `[βˆ€ 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.
204204
-/
205205
def toTruncate [HasZeroObject V] [HasZeroMorphisms V] (C : CochainComplex V β„•) :
206206
(singleβ‚€ V).obj (C.X 0) ⟢ truncate.obj C :=
207-
(fromSingleβ‚€Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 0 1, by aesop⟩
207+
(fromSingleβ‚€Equiv (truncate.obj C) (C.X 0)).symm ⟨C.d 0 1, by simp⟩
208208

209209
variable [HasZeroMorphisms V]
210210

β€ŽMathlib/Algebra/Homology/HomologicalBicomplex.leanβ€Ž

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -177,15 +177,15 @@ def flipEquivalenceUnitIso :
177177
𝟭 (HomologicalComplexβ‚‚ C c₁ cβ‚‚) β‰… flipFunctor C c₁ cβ‚‚ β‹™ flipFunctor C cβ‚‚ c₁ :=
178178
NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun i₁ =>
179179
HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
180-
(by aesop_cat)) (by aesop_cat)) (by aesop_cat)
180+
(by simp)) (by aesop_cat)) (by aesop_cat)
181181

182182
/-- Auxiliary definition for `HomologicalComplexβ‚‚.flipEquivalence`. -/
183183
@[simps!]
184184
def flipEquivalenceCounitIso :
185185
flipFunctor C cβ‚‚ c₁ β‹™ flipFunctor C c₁ cβ‚‚ β‰… 𝟭 (HomologicalComplexβ‚‚ C cβ‚‚ c₁) :=
186186
NatIso.ofComponents (fun K => HomologicalComplex.Hom.isoOfComponents (fun iβ‚‚ =>
187187
HomologicalComplex.Hom.isoOfComponents (fun _ => Iso.refl _)
188-
(by aesop_cat)) (by aesop_cat)) (by aesop_cat)
188+
(by simp)) (by aesop_cat)) (by aesop_cat)
189189

190190
/-- Flipping a complex of complexes over the diagonal, as an equivalence of categories. -/
191191
@[simps]

β€ŽMathlib/Algebra/Homology/HomologySequence.leanβ€Ž

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -165,7 +165,7 @@ noncomputable def composableArrows₃Functor [CategoryWithHomology C] :
165165
HomologicalComplex C c β₯€ ComposableArrows C 3 where
166166
obj K := composableArrows₃ K i j
167167
map {K L} Ο† := ComposableArrows.homMk₃ (homologyMap Ο† i) (opcyclesMap Ο† i) (cyclesMap Ο† j)
168-
(homologyMap Ο† j) (by aesop_cat) (by aesop_cat) (by aesop_cat)
168+
(homologyMap Ο† j) (by simp) (by simp) (by simp)
169169

170170
end HomologySequence
171171

@@ -311,7 +311,7 @@ lemma homology_exactβ‚‚ : (ShortComplex.mk (HomologicalComplex.homologyMap S.f i
311311
have e : S.map (HomologicalComplex.homologyFunctor C c i) β‰…
312312
S.map (HomologicalComplex.opcyclesFunctor C c i) :=
313313
ShortComplex.isoMk (asIso (S.X₁.homologyΞΉ i))
314-
(asIso (S.Xβ‚‚.homologyΞΉ i)) (asIso (S.X₃.homologyΞΉ i)) (by aesop_cat) (by aesop_cat)
314+
(asIso (S.Xβ‚‚.homologyΞΉ i)) (asIso (S.X₃.homologyΞΉ i)) (by simp) (by simp)
315315
exact ShortComplex.exact_of_iso e.symm (opcycles_right_exact S hS.exact i)
316316

317317
/-- Exactness of `S.Xβ‚‚.homology i ⟢ S.X₃.homology i ⟢ S.X₁.homology j`. -/

β€ŽMathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -201,7 +201,7 @@ noncomputable def triangleRotateIsoTriangleOfDegreewiseSplit :
201201
(triangle Ο†).rotate β‰…
202202
triangleOfDegreewiseSplit _ (triangleRotateShortComplexSplitting Ο†) :=
203203
Triangle.isoMk _ _ (Iso.refl _) (Iso.refl _) (Iso.refl _)
204-
(by aesop_cat) (by aesop_cat) (by ext; dsimp; simp)
204+
(by simp) (by simp) (by ext; dsimp; simp)
205205

206206
/-- The triangle `(triangleh Ο†).rotate` is isomorphic to a triangle attached to a
207207
degreewise split short exact sequence of cochain complexes. -/

β€ŽMathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.leanβ€Ž

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -50,9 +50,9 @@ def inverse : (J β₯€ ShortComplex C) β₯€ ShortComplex (J β₯€ C) where
5050
@[simps!]
5151
def unitIso : 𝟭 _ β‰… functor J C β‹™ inverse J C :=
5252
NatIso.ofComponents (fun _ => isoMk
53-
(NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
54-
(NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
55-
(NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat))
53+
(NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
54+
(NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
55+
(NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
5656
(by aesop_cat) (by aesop_cat)) (by aesop_cat)
5757

5858
/-- The counit isomorphism of the equivalence
@@ -61,7 +61,7 @@ def unitIso : 𝟭 _ β‰… functor J C β‹™ inverse J C :=
6161
def counitIso : inverse J C β‹™ functor J C β‰… 𝟭 _ :=
6262
NatIso.ofComponents (fun _ => NatIso.ofComponents
6363
(fun _ => isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
64-
(by aesop_cat) (by aesop_cat)) (by aesop_cat)) (by aesop_cat)
64+
(by simp) (by simp)) (by aesop_cat)) (by aesop_cat)
6565

6666
end FunctorEquivalence
6767

β€ŽMathlib/Algebra/Homology/ShortComplex/HomologicalComplex.leanβ€Ž

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -50,7 +50,7 @@ when `c.prev j = i` and `c.next j = k`. -/
5050
noncomputable def natIsoSc' (i j k : ΞΉ) (hi : c.prev j = i) (hk : c.next j = k) :
5151
shortComplexFunctor C c j β‰… shortComplexFunctor' C c i j k :=
5252
NatIso.ofComponents (fun K => ShortComplex.isoMk (K.XIsoOfEq hi) (Iso.refl _) (K.XIsoOfEq hk)
53-
(by aesop_cat) (by aesop_cat)) (by aesop_cat)
53+
(by simp) (by simp)) (by aesop_cat)
5454

5555
variable {C c}
5656

0 commit comments

Comments
Β (0)