awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
f : PolynomialModule R M
hf : f ∈ F.submodule.toAddSubmonoid
⊢ Membership.mem (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.sum f Finsupp.single)
have apply : ∀ c ∈ f.support,
  Membership.mem (α := PolynomialModule R M) (γ := AddSubmonoid (PolynomialModule R M))
    (AddSubmonoid.closure (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)))
    (Finsupp.single c ((f : (a : ℕ) → M) c) : ℕ →₀ M)
Tactic: apply AddSubmonoid.sum_mem _ _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
⊢ Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) =
    F.submodule
have rw : Submodule.span ↥(reesAlgebra I) (↑F.submodule : Set (PolynomialModule R M)) = F.submodule
Tactic: rw [← Submodule.span_closure, submodule_closure_single, Submodule.coe_toAddSubmonoid]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
have rw : (∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))) ↔
  ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
Tactic: rw [← submodule_span_single,
    ← (Submodule.span_mono (Set.iUnion₂_subset_iUnion _ _)).ge_iff_eq',
    Submodule.span_le, Set.iUnion_subset_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
⊢ (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
have mp : (∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))) →
  ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
mp :
  (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) →
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
⊢ (∀ (i : ℕ),
      (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
        (↑(Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
          Set (PolynomialModule R M))) ↔
    ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
have mpr : (∀ n ≥ n₀, I • F.N n = F.N (n + 1)) →
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
⊢ I • F.N n = F.N (n + 1)
have mp : F.N (n + 1) ≤ I • F.N n
Tactic: refine (F.smul_le n).antisymm ?_
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
⊢ x ∈ I • F.N n
have mp : ∀
  (l :
    Finsupp.{u_2, u_1}
      (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
      ↥(reesAlgebra I))
  (hl :
    Eq.{u_2 + 1} (α := PolynomialModule R M)
      ((Finsupp.linearCombination (↥(reesAlgebra I))
              (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                  x)) :
            (a :
                (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                    Type u_2) →₀
                  ↥(reesAlgebra I)) →
              PolynomialModule R M)
          l :
        PolynomialModule R M)
      ((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)),
  x ∈ I • F.N n
Tactic: obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_linearCombination _ _ _).mp (H _ ⟨x, hx, rfl⟩)
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  Eq.{u_2 + 1} (α := PolynomialModule R M)
    ((Finsupp.linearCombination (↥(reesAlgebra I))
            (Subtype.val (p := fun (x : PolynomialModule R M) ↦
              Membership.mem (γ := Set (PolynomialModule R M))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                x)) :
          (a :
              (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                  Type u_2) →₀
                ↥(reesAlgebra I)) →
            PolynomialModule R M)
        l :
      PolynomialModule R M)
    ((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)
⊢ x ∈ I • F.N n
have hl₁ : Eq.{u_2 + 1} (α := M)
  ((fun (f : ℕ →₀ M) ↦ ((f : (a : ℕ) → M) (n + 1) : M))
    ((Finsupp.linearCombination (↥(reesAlgebra I))
          (Subtype.val (p := fun (x : PolynomialModule R M) ↦
            Membership.mem (γ := Set (PolynomialModule R M))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)) :
        (a :
            (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                Type u_2) →₀
              ↥(reesAlgebra I)) →
          PolynomialModule R M)
      l))
  ((fun (f : ℕ →₀ M) ↦ ((f : (a : ℕ) → M) (n + 1) : M)) ((single R (n + 1) : (a : M) → PolynomialModule R M) x))
Tactic: replace hl := congr_arg (fun f : ℕ →₀ M => f (n + 1)) hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  Eq (α := M)
    ((((Finsupp.linearCombination (↥(reesAlgebra I))
                  (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                    Membership.mem (γ := Set (PolynomialModule R M))
                      (⋃ (i : ℕ),
                        ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                      x)) :
                (a :
                    (↑(⋃ (i : ℕ),
                            ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                        Type u_2) →₀
                      ↥(reesAlgebra I)) →
                  PolynomialModule R M)
              l :
            PolynomialModule R M) :
          (a : ℕ) → M)
        (n + 1) :
      M)
    ((((single R (n + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M) : (a : ℕ) → M) (n + 1) : M)
⊢ x ∈ I • F.N n
have hl₁ : (((Finsupp.linearCombination (↥(reesAlgebra I))
              (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                  x)) :
            (a :
                (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                    Type u_2) →₀
                  ↥(reesAlgebra I)) →
              PolynomialModule R M)
          l :
        PolynomialModule R M) :
      (a : ℕ) → M)
    (n + 1) =
  x
Tactic: rw [PolynomialModule.single_apply, if_pos rfl] at hl
Cleared hypotheses: hl
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
⊢ x ∈ I • F.N n
have mp : (l.sum
    fun
      (a₁ :
        (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
          Type u_2))
      (b : ↥(reesAlgebra I)) ↦
    (b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1)) ∈
  I • F.N n
Tactic: rw [← hl, Finsupp.linearCombination_apply, Finsupp.sum_apply]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
⊢ (l.sum
      fun
        (a₁ :
          (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
            Type u_2))
        (b : ↥(reesAlgebra I)) ↦
      (b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1)) ∈
    I • F.N n
have apply : ∀ c ∈ l.support,
  (fun
          (a₁ :
            (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
              Type u_2))
          (b : ↥(reesAlgebra I)) ↦
        ((b • (↑a₁ : PolynomialModule R M) : (a : ℕ) → M) (n + 1) : M))
      c
      ((l :
          (a :
              (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                Type u_2)) →
            ↥(reesAlgebra I))
        c) ∈
    I • F.N n
Tactic: apply Submodule.sum_mem _ _
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
⊢ Membership.mem (α := M) (I • F.N n)
    ((HSMul.hSMul.{u_1, u_2, u_2} (α := ↥(reesAlgebra I)) (β := PolynomialModule R M)
            ((l :
                  (a :
                      (↑(⋃ (i : ℕ),
                            ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                        Type u_2)) →
                    ↥(reesAlgebra I))
                (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)
                  ((single R n' : (a : M) → PolynomialModule R M) m) ⋯) :
              ↥(reesAlgebra I))
            ((single R n' : (a : M) → PolynomialModule R M) m : PolynomialModule R M) :
          (a : ℕ) → M)
        (n + 1) :
      M)
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := R)
    (coeff
      (↑((l :
              (a :
                  (↑(⋃ (i : ℕ),
                        ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                    Type u_2)) →
                ↥(reesAlgebra I))
            (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
              Membership.mem (γ := Set (PolynomialModule R M))
                (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
              ((single R n' : (a : M) → PolynomialModule R M) m) sorry)) :
        R[X])
      (n + 1 - n'))
    m ∈
  I • F.N n
Tactic: rw [Subalgebra.smul_def, smul_single_apply, if_pos (show n' ≤ n + 1 by lia)]
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (coeff
        (↑((l :
                (a :
                    (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2)) →
                  ↥(reesAlgebra I))
              (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
                ((single R n' : (a : M) → PolynomialModule R M) m) ⋯)) :
          R[X])
        (n + 1 - n'))
      m ∈
    I • F.N n
have e : n' ≤ n
Tactic: have e : n' ≤ n := by lia
-- Lean 4 proof step from Mathlib.RingTheory.Filtration (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑(Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) :
        Set (PolynomialModule R M))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l :
  Finsupp.{u_2, u_1}
    (↑(⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) : Type u_2)
    ↥(reesAlgebra I)
hl :
  (((Finsupp.linearCombination (↥(reesAlgebra I))
                (Subtype.val (p := fun (x : PolynomialModule R M) ↦
                  Membership.mem (γ := Set (PolynomialModule R M))
                    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
                    x)) :
              (a :
                  (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2) →₀
                    ↥(reesAlgebra I)) →
                PolynomialModule R M)
            l :
          PolynomialModule R M) :
        (a : ℕ) → M)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ (↑(F.N n') : Set M)
e : n' ≤ n
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := R)
      (coeff
        (↑((l :
                (a :
                    (↑(⋃ (i : ℕ),
                          ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                      Type u_2)) →
                  ↥(reesAlgebra I))
              (Subtype.mk (p := fun (x : PolynomialModule R M) ↦
                Membership.mem (γ := Set (PolynomialModule R M))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) x)
                ((single R n' : (a : M) → PolynomialModule R M) m) ⋯)) :
          R[X])
        (n + 1 - n'))
      m ∈
    I • F.N n
have this : I ^ (n - n' + 1) • F.N n' ≤ HPow.hPow (β := ℕ) I 1 • F.N (n - n' + n')
Tactic: have := F.pow_smul_le_pow_smul (n - n') n' 1