R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) ↔
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)

R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ≤
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ Filtration.submodule F =
      Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ↔
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
rw [← submodule_span_single, ← LE.le.le_iff_eq, Submodule.span_le, Set.iUnion_subset_iff]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ≤
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))

R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) ↔
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) ↔
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)

R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ≤
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
swap
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) →
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)

case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)) →
    ∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) ↔
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
constructor
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ≤
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
exact Submodule.span_mono (Set.iUnion₂_subset_iUnion _ _)
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
⊢ I • N F n = N F (n + 1)
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))) →
    ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
intro H n hn
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
⊢ N F (n + 1) ≤ I • N F n
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
⊢ I • N F n = N F (n + 1)
refine' (F.smul_le n).antisymm _
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
⊢ x ∈ I • N F n
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
⊢ N F (n + 1) ≤ I • N F n
intro x hx
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
          { x // x ∈ reesAlgebra I } Subtype.val)
      l =
    ↑(single R (n + 1)) x
⊢ x ∈ I • N F n
case mp
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
⊢ x ∈ I • N F n
obtain ⟨l, hl⟩ := (Finsupp.mem_span_iff_total _ _ _).mp (H _ ⟨x, hx, rfl⟩)
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  (fun f => ↑f (n + 1))
      (↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
            { x // x ∈ reesAlgebra I } Subtype.val)
        l) =
    (fun f => ↑f (n + 1)) (↑(single R (n + 1)) x)
⊢ x ∈ I • N F n
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
          { x // x ∈ reesAlgebra I } Subtype.val)
      l =
    ↑(single R (n + 1)) x
⊢ x ∈ I • N F n
replace hl := congr_arg (fun f : ℕ →₀ M => f (n + 1)) hl
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    ↑(↑(single R (n + 1)) x) (n + 1)
⊢ x ∈ I • N F n
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  (fun f => ↑f (n + 1))
      (↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
            { x // x ∈ reesAlgebra I } Subtype.val)
        l) =
    (fun f => ↑f (n + 1)) (↑(single R (n + 1)) x)
⊢ x ∈ I • N F n
dsimp only at hl
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ x ∈ I • N F n
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    ↑(↑(single R (n + 1)) x) (n + 1)
⊢ x ∈ I • N F n
erw [Finsupp.single_eq_same] at hl
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ (Finsupp.sum l fun a₁ b => ↑(b • ↑a₁) (n + 1)) ∈ I • N F n
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ x ∈ I • N F n
rw [← hl, Finsupp.total_apply, Finsupp.sum_apply]
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ ∀ (c : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))),
    c ∈ l.support → (fun a₁ b => ↑(b • ↑a₁) (n + 1)) c (↑l c) ∈ I • N F n
case mp.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ (Finsupp.sum l fun a₁ b => ↑(b • ↑a₁) (n + 1)) ∈ I • N F n
apply Submodule.sum_mem _ _
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ (fun a₁ b => ↑(b • ↑a₁) (n + 1))
      { val := ↑(single R n') m,
        property :=
          (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }
      (↑l
        { val := ↑(single R n') m,
          property :=
            (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }) ∈
    I • N F n
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
⊢ ∀ (c : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))),
    c ∈ l.support → (fun a₁ b => ↑(b • ↑a₁) (n + 1)) c (↑l c) ∈ I • N F n
rintro ⟨_, _, ⟨n', rfl⟩, _, ⟨hn', rfl⟩, m, hm, rfl⟩ -
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ ↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) } •
          ↑(single R n') m)
      (n + 1) ∈
    I • N F n
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ (fun a₁ b => ↑(b • ↑a₁) (n + 1))
      { val := ↑(single R n') m,
        property :=
          (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }
      (↑l
        { val := ↑(single R n') m,
          property :=
            (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }) ∈
    I • N F n
dsimp only [Subtype.coe_mk]
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ ↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) } •
          ↑(single R n') m)
      (n + 1) ∈
    I • N F n
rw [Subalgebra.smul_def, smul_single_apply, if_pos (show n' ≤ n + 1 by linarith)]
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
have e : n' ≤ n := by linarith
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
this : I ^ (n - n' + 1) • N F n' ≤ I ^ 1 • N F (n - n' + n')
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
have := F.pow_smul_le_pow_smul (n - n') n' 1
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
this : I ^ (n + 1 - n') • N F n' ≤ I • N F n
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
this : I ^ (n - n' + 1) • N F n' ≤ I ^ 1 • N F (n - n' + n')
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
rw [tsub_add_cancel_of_le e, pow_one, add_comm _ 1, ← add_tsub_assoc_of_le e, add_comm] at this
no goals
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
e : n' ≤ n
this : I ^ (n + 1 - n') • N F n' ≤ I • N F n
⊢ coeff
        (↑(↑l
            { val := ↑(single R n') m,
              property :=
                (_ : ∃ t, (t ∈ Set.range fun i => ⋃ (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) ∧ ↑(single R n') m ∈ t) }))
        (n + 1 - n') •
      m ∈
    I • N F n
exact this (Submodule.smul_mem_smul ((l _).2 <| n + 1 - n') hm)
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ n' ≤ n + 1
linarith
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ↑(single R i) '' ↑(N F i) ⊆
      ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ N F (n + 1)
l : ↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)) →₀ { x // x ∈ reesAlgebra I }
hl :
  ↑(↑(Finsupp.total (↑(⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) (PolynomialModule R M)
              { x // x ∈ reesAlgebra I } Subtype.val)
          l)
      (n + 1) =
    x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(N F n')
⊢ n' ≤ n
linarith
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
⊢ (∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)) →
    ∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
h : Stable F
n₀ : ℕ
⊢ (∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)) →
    ∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
let F' := Submodule.span (reesAlgebra I) (⋃ i ≤ n₀, single R i '' (F.N i : Set M))
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i : ℕ
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
⊢ (∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)) →
    ∀ (i : ℕ),
      ↑(single R i) '' ↑(N F i) ⊆
        ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
intro hF i
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i : ℕ
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i : ℕ
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
have : ∀ i ≤ n₀, single R i '' (F.N i : Set M) ⊆ F' := by
  intro i hi
  refine Set.Subset.trans ?_ Submodule.subset_span
  refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
  exact hi
case mpr.zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
⊢ ↑(single R Nat.zero) '' ↑(N F Nat.zero) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))

case mpr.succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case mpr
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i : ℕ
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
induction' i with j hj
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : Nat.succ j ≤ n₀
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))

case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : ¬Nat.succ j ≤ n₀
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case mpr.succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
by_cases hj' : j.succ ≤ n₀
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : ¬Nat.succ j ≤ n₀
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
simp only [not_le, Nat.lt_succ_iff] at hj'
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
⊢ ↑(single R (j + 1)) '' ↑(I • N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
rw [Nat.succ_eq_add_one, ← hF _ hj']
case neg.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
⊢ ↑(single R (j + 1)) m ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
⊢ ↑(single R (j + 1)) '' ↑(I • N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
rintro _ ⟨m, hm, rfl⟩
case neg.intro.intro.refine'_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ N F j
⊢ ↑(single R (j + 1)) (r • m') ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))

case neg.intro.intro.refine'_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
x y : M
hx :
  ↑(single R (j + 1)) x ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hy :
  ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (j + 1)) (x + y) ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg.intro.intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
⊢ ↑(single R (j + 1)) m ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
refine' Submodule.smul_induction_on hm (fun r hr m' hm' => _) (fun x y hx hy => _)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ ↑(single R i) '' ↑(N F i) ⊆ ↑F'
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i : ℕ
⊢ ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
intro i hi
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ ↑(single R i) '' ↑(N F i) ⊆ ⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ ↑(single R i) '' ↑(N F i) ⊆ ↑F'
refine Set.Subset.trans ?_ Submodule.subset_span
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ i ≤ n₀
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ ↑(single R i) '' ↑(N F i) ⊆ ⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)
refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ i ≤ n₀
exact hi
no goals
case mpr.zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
⊢ ↑(single R Nat.zero) '' ↑(N F Nat.zero) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
exact this _ (zero_le _)
no goals
case pos
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : Nat.succ j ≤ n₀
⊢ ↑(single R (Nat.succ j)) '' ↑(N F (Nat.succ j)) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
exact this _ hj'
case neg.intro.intro.refine'_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ N F j
⊢ ↑(monomial 1) r • ↑(single R j) m' ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg.intro.intro.refine'_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ N F j
⊢ ↑(single R (j + 1)) (r • m') ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
rw [add_comm, ← monomial_smul_single]
no goals
case neg.intro.intro.refine'_1
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ N F j
⊢ ↑(monomial 1) r • ↑(single R j) m' ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
exact F'.smul_mem
  ⟨_, reesAlgebra.monomial_mem.mpr (by rwa [pow_one])⟩ (hj <| Set.mem_image_of_mem _ hm')
no goals
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
r : R
hr : r ∈ I
m' : M
hm' : m' ∈ N F j
⊢ r ∈ I ^ 1
rwa [pow_one]
case neg.intro.intro.refine'_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
x y : M
hx :
  ↑(single R (j + 1)) x ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hy :
  ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (j + 1)) x + ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
case neg.intro.intro.refine'_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
x y : M
hx :
  ↑(single R (j + 1)) x ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hy :
  ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (j + 1)) (x + y) ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
rw [map_add]
no goals
case neg.intro.intro.refine'_2
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F'✝ : Filtration I M
h : Stable F
n₀ : ℕ
F' : Submodule { x // x ∈ reesAlgebra I } (PolynomialModule R M) :=
  Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
hF : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
this : ∀ (i : ℕ), i ≤ n₀ → ↑(single R i) '' ↑(N F i) ⊆ ↑F'
j : ℕ
hj :
  ↑(single R j) '' ↑(N F j) ⊆
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • N F j)
x y : M
hx :
  ↑(single R (j + 1)) x ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
hy :
  ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
⊢ ↑(single R (j + 1)) x + ↑(single R (j + 1)) y ∈
    ↑(Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)))
exact F'.add_mem hx hy