awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this : I ^ (n - n' + 1) • F.N n' ≤ HPow.hPow (β := ℕ) I 1 • F.N (n - 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 + 1 - n') • F.N n' ≤ I • F.N n
Tactic: rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this
Cleared hypotheses: this
-- 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₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ 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))
have this : ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
Tactic: have : ∀ i ≤ n₀, single R i '' (F.N i : Set M) ⊆ F' := fun i hi =>
      -- Porting note: need to add hint for `s`
      (Set.subset_iUnion₂ (s := fun i _ => (single R i '' (N F i : Set M))) i hi).trans
        Submodule.subset_span
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
i : ℕ
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
⊢ (⇑(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))
have mpr : ∀ (j : ℕ)
  (hj :
    (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))),
  (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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: induction i with
    | zero => exact this _ zero_le
    | succ j hj => ?_
Cleared hypotheses: i
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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))
have pos : ∀ (hj' : j.succ ≤ n₀),
  (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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: by_cases hj' : j.succ ≤ n₀
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
pos :
  ∀ (hj' : j.succ ≤ n₀),
    (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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))
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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))
have neg : ∀ (hj' : ¬j.succ ≤ n₀),
  (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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: by_cases hj' : j.succ ≤ n₀
-- 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₀ : ℕ
F' : Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : ¬j.succ ≤ n₀
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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))
have hj'₁ : n₀ ≤ j
Tactic: simp only [not_le, Nat.lt_succ_iff] at hj'
Cleared hypotheses: hj'
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : n₀ ≤ j
⊢ (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(F.N (j + 1)) : 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))
have neg : (⇑(single R (j + 1)) : (a : M) → PolynomialModule R M) '' (↑(I • F.N j) : 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: rw [← hF _ hj']
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : n₀ ≤ j
m : M
hm : m ∈ (↑(I • F.N j) : Set M)
⊢ Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
have neg : ∀ (r : R) (hr : r ∈ I) (m' : M) (hm' : m' ∈ F.N j),
  Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) (r • m') : PolynomialModule R M)
Tactic: refine Submodule.smul_induction_on hm (fun r hr m' hm' => ?_) (fun x y hx hy => ?_)
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : n₀ ≤ j
m : M
hm : m ∈ (↑(I • F.N j) : Set M)
neg :
  ∀ (r : R) (hr : r ∈ I) (m' : M) (hm' : m' ∈ F.N j),
    Membership.mem (α := PolynomialModule R 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))
      ((single R (j + 1) : (a : M) → PolynomialModule R M) (r • m') : PolynomialModule R M)
⊢ Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) m : PolynomialModule R M)
have neg₁ : ∀ (x y : M)
  (hx :
    Membership.mem (α := PolynomialModule R 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))
      ((single R (j + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M))
  (hy :
    Membership.mem (α := PolynomialModule R 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))
      ((single R (j + 1) : (a : M) → PolynomialModule R M) y : PolynomialModule R M)),
  Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) (x + y) : PolynomialModule R M)
Tactic: refine Submodule.smul_induction_on hm (fun r hr m' hm' => ?_) (fun x y hx hy => ?_)
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : n₀ ≤ j
m : M
hm : m ∈ (↑(I • F.N j) : Set M)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ F.N j
⊢ Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) (r • m') : PolynomialModule R M)
have neg : HSMul.hSMul (α := R[X]) (β := PolynomialModule R M) ((monomial 1 : (a : R) → R[X]) r : R[X])
    ((single R j : (a : M) → PolynomialModule R M) m' : PolynomialModule R 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: rw [add_comm, ← monomial_smul_single]
-- 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.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this :
  ∀ i ≤ n₀, (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆ (↑F' : Set (PolynomialModule R M))
j : ℕ
hj :
  (⇑(single R j) : (a : M) → PolynomialModule R M) '' (↑(F.N j) : 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))
hj' : n₀ ≤ j
m : M
hm : m ∈ (↑(I • F.N j) : Set M)
x y : M
hx :
  Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)
hy :
  Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) y : PolynomialModule R M)
⊢ Membership.mem (α := PolynomialModule R 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))
    ((single R (j + 1) : (a : M) → PolynomialModule R M) (x + y) : PolynomialModule R M)
have neg : HAdd.hAdd (α := PolynomialModule R M) (β := PolynomialModule R M)
    ((single R (j + 1) : (a : M) → PolynomialModule R M) x : PolynomialModule R M)
    ((single R (j + 1) : (a : M) → PolynomialModule R M) y : PolynomialModule R 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: rw [map_add]
-- 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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
have simp_rw : F.submodule.FG ↔
  ∃ (n₀ : ℕ),
    F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
Tactic: simp_rw [← F.submodule_eq_span_le_iff_stable_ge]
-- 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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔
    ∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
have mp : F.submodule.FG →
  ∃ (n₀ : ℕ),
    F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set 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
hF' : ∀ (i : ℕ), (F.N i).FG
mp :
  F.submodule.FG →
    ∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
⊢ F.submodule.FG ↔
    ∃ (n₀ : ℕ),
      F.submodule =
        Submodule.span (↥(reesAlgebra I))
          (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
have mpr : (∃ (n₀ : ℕ),
    F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))) →
  F.submodule.FG
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ ∃ (n₀ : ℕ),
    F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
have mp : Monotone.{0, u_2} (β := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)) fun (n₀ : ℕ) ↦
  Submodule.span (↥(reesAlgebra I))
    (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
Tactic: refine H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_
-- 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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
mp :
  Monotone.{0, u_2} (β := Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)) fun (n₀ : ℕ) ↦
    Submodule.span (↥(reesAlgebra I))
      (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
⊢ ∃ (n₀ : ℕ),
    F.submodule =
      Submodule.span (↥(reesAlgebra I))
        (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M))
have mp₁ : iSup (ι := ℕ)
    (⇑{
          toFun := fun (n₀ : ℕ) ↦
            Submodule.span (↥(reesAlgebra I))
              (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)),
          monotone' := sorry } :
      (a : ℕ) → Submodule (↥(reesAlgebra I)) (PolynomialModule R M)) =
  F.submodule
Tactic: refine H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_