Merge branch 'vi.limitLemmas' into vi.normal

.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/[email protected]
-        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

.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/[email protected]
-        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

.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/[email protected]
-        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

.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/[email protected]
-        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)

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

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

Mathlib/Algebra/Category/ModuleCat/Subobject.lean

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

Mathlib/Algebra/Category/Semigrp/Basic.lean

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

Mathlib/Algebra/Homology/Additive.lean

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

Mathlib/Algebra/Homology/Augment.lean

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

Mathlib/Algebra/Homology/HomologicalBicomplex.lean

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

Mathlib/Algebra/Homology/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 :=

Mathlib/Algebra/Homology/HomologySequence.lean

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

Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean

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

Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean

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

Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean

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

Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean

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

Mathlib/Algebra/Homology/ShortComplex/Limits.lean

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

Mathlib/Algebra/Homology/ShortComplex/PreservesHomology.lean

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

Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

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

Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

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

Mathlib/Algebra/Homology/Single.lean

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

Mathlib/Algebra/Lie/Weights/Basic.lean

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

Mathlib/Algebra/Module/Presentation/Basic.lean

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

Mathlib/Algebra/Module/Submodule/Pointwise.lean

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