awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Filtration
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))

Tactic:
this _ hj'
-- Module: Mathlib.RingTheory.Filtration
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))

Tactic:
exact this _ hj'
-- Module: Mathlib.RingTheory.Filtration
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₀
⊢ n₀ ≤ j

Tactic:
simp only [not_le, Nat.lt_succ_iff] at hj'

Premises used: not_le, Nat.lt_succ_iff
-- Module: Mathlib.RingTheory.Filtration
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
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))
⊢ (⇑(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:
rw [← hF _ hj']
-- Module: Mathlib.RingTheory.Filtration
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)

Tactic:
Submodule.smul_induction_on hm (fun r hr m' hm' => ?_) (fun x y hx hy => ?_)

Premises used: Submodule.smul_induction_on
-- Module: Mathlib.RingTheory.Filtration
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)
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)
⊢ 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)

Tactic:
refine Submodule.smul_induction_on hm (fun r hr m' hm' => ?_) (fun x y hx hy => ?_)
-- Module: Mathlib.RingTheory.Filtration
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
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))
⊢ 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:
rw [add_comm, ← monomial_smul_single]

Premises used: PolynomialModule.monomial_smul_single, add_comm
-- Module: Mathlib.RingTheory.Filtration
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
rwa rwa₁ rwa₂ rwa₃ : r ∈ I
⊢ r ∈ HPow.hPow (β := ℕ) I 1

Tactic:
rwa [pow_one]

Premises used: pow_one
-- Module: Mathlib.RingTheory.Filtration
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
⊢ 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:
exact F'.smul_mem
        ⟨_, reesAlgebra.monomial_mem.mpr (by rwa [pow_one])⟩ (hj <| Set.mem_image_of_mem _ hm')

Premises used: Iff.mpr, reesAlgebra.monomial_mem, Subtype.mk, Set.mem_image_of_mem, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Filtration
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)
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))
⊢ 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:
rw [map_add]

Premises used: map_add
-- Module: Mathlib.RingTheory.Filtration
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)
⊢ 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:
F'.add_mem hx hy

Premises used: Set.Mem, Submodule.add_mem
-- Module: Mathlib.RingTheory.Filtration
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)
⊢ 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:
exact F'.add_mem hx hy

Premises used: Submodule.add_mem
-- Module: Mathlib.RingTheory.Filtration
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
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))
⊢ F.submodule.FG ↔ ∃ (n₀ : ℕ), ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Tactic:
simp_rw [← F.submodule_eq_span_le_iff_stable_ge]

Premises used: Ideal.Filtration.submodule_eq_span_le_iff_stable_ge
-- Module: Mathlib.RingTheory.Filtration
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))
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
⊢ 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
-- Module: Mathlib.RingTheory.Filtration
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))

Tactic:
H.stabilizes_of_iSup_eq
        ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), ?_⟩ ?_

Premises used: Membership.mem, PolynomialModule.single, Subtype, Submodule.FG.stabilizes_of_iSup_eq, SetLike.coe, Submodule.span, Ideal.Filtration.N, OrderHom.mk, Set.image, DFunLike.coe, Set.iUnion, reesAlgebra
-- Module: Mathlib.RingTheory.Filtration
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))
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' := ⋯ } :
        (a : ℕ) → Submodule (↥(reesAlgebra I)) (PolynomialModule R M)) =
    F.submodule
⊢ ∃ (n₀ : ℕ),
    F.submodule =
      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)), ?_⟩ ?_

Premises used: Membership.mem, PolynomialModule.single, Subtype, Submodule.FG.stabilizes_of_iSup_eq, SetLike.coe, Submodule.span, Ideal.Filtration.N, OrderHom.mk, Set.image, DFunLike.coe, Set.iUnion, reesAlgebra
-- Module: Mathlib.RingTheory.Filtration
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 m : ℕ
e : n ≤ m
mp :
  ∀ (i : ℕ) (j : i ≤ n),
    (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M) ⊆
      (↑((fun (n₀ : ℕ) ↦
              (Submodule.span (↥(reesAlgebra I))
                  (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
                Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)))
            m) :
        Set (PolynomialModule R M))
⊢ LE.le.{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)) :
          Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)))
      n)
    ((fun (n₀ : ℕ) ↦
        (Submodule.span (↥(reesAlgebra I))
            (⋃ (i : ℕ), ⋃ (_ : i ≤ n₀), (⇑(single R i) : (a : M) → PolynomialModule R M) '' (↑(F.N i) : Set M)) :
          Submodule.{u_1, u_2} (↥(reesAlgebra I)) (PolynomialModule R M)))
      m)

Tactic:
rw [Submodule.span_le, Set.iUnion₂_subset_iff]

Premises used: Set.iUnion₂_subset_iff, Submodule.span_le