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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) ↔ ∃ n₀, ∀ (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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) ↔ Stable F
delta Ideal.Filtration.Stable
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) ↔
    ∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) ↔ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
simp_rw [← F.submodule_eq_span_le_iff_stable_ge]
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) →
    ∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ (∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))) →
    Submodule.FG (Filtration.submodule 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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) ↔
    ∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))
constructor
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ ∃ n₀,
    Filtration.submodule F =
      Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ Submodule.FG (Filtration.submodule F) →
    ∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))
rintro H
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ iSup
      ↑{
          toFun := fun n₀ =>
            Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)),
          monotone' := ?m.295545 } =
    Filtration.submodule 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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ Monotone fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ ∃ n₀,
    Filtration.submodule F =
      Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))
apply H.stablizes_of_iSup_eq
    ⟨fun n₀ => Submodule.span _ (⋃ (i : ℕ) (_ : i ≤ n₀), single R i '' ↑(F.N i)), _⟩
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ (⨆ (n₀ : ℕ), Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) =
    Filtration.submodule F
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ iSup
      ↑{
          toFun := fun n₀ =>
            Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i)),
          monotone' := ?m.295545 } =
    Filtration.submodule F
dsimp
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ (⨆ (n₀ : ℕ), Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) =
    Filtration.submodule F
rw [← Submodule.span_iUnion, ← submodule_span_single]
case mp.e_s
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ (⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) = ⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ), ↑(single R i) '' ↑(N F i))
congr 1
case mp.e_s.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (x✝ ∈ ⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) ↔ x✝ ∈ ⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)
case mp.e_s
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ (⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) = ⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)
ext
case mp.e_s.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝) ↔ ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝
case mp.e_s.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (x✝ ∈ ⋃ (i : ℕ) (i_1 : ℕ) (_ : i_1 ≤ i), ↑(single R i_1) '' ↑(N F i_1)) ↔ x✝ ∈ ⋃ (i : ℕ), ↑(single R i) '' ↑(N F i)
simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, exists_prop]
case mp.e_s.h.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝) → ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝

case mp.e_s.h.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝) → ∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝
case mp.e_s.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝) ↔ ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝
constructor
case mp.e_s.h.mp.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x, x ∈ N F i ∧ ↑(single R i) x = x✝
⊢ ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝
case mp.e_s.h.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝) → ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝
rintro ⟨-, i, -, e⟩
no goals
case mp.e_s.h.mp.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x, x ∈ N F i ∧ ↑(single R i) x = x✝
⊢ ∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝
exact ⟨i, e⟩
case mp.e_s.h.mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x, x ∈ N F i ∧ ↑(single R i) x = x✝
⊢ ∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝
case mp.e_s.h.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
⊢ (∃ i x, x ∈ N F i ∧ ↑(single R i) x = x✝) → ∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝
rintro ⟨i, e⟩
no goals
case mp.e_s.h.mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x, x ∈ N F i ∧ ↑(single R i) x = x✝
⊢ ∃ i i_1, i_1 ≤ i ∧ ∃ x, x ∈ N F i_1 ∧ ↑(single R i_1) x = x✝
exact ⟨i, i, le_refl i, e⟩
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
⊢ (fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) n ≤
    (fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
⊢ Monotone fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))
intro n m e
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
⊢ ∀ (i : ℕ),
    i ≤ n →
      ↑(single R i) '' ↑(N F i) ⊆
        ↑((fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
⊢ (fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) n ≤
    (fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m
rw [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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑((fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
⊢ ∀ (i : ℕ),
    i ≤ n →
      ↑(single R i) '' ↑(N F i) ⊆
        ↑((fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ↑(single R i) '' ↑(N F i) ⊆ ⋃ (i : ℕ) (_ : i ≤ m), ↑(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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ↑(single R i) '' ↑(N F i) ⊆
    ↑((fun n₀ => Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), ↑(single R i) '' ↑(N F i))) m)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ↑(single R i) '' ↑(N F i) ⊆ ⋃ (i : ℕ) (_ : i ≤ m), ↑(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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
H : Submodule.FG (Filtration.submodule F)
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m
exact hi.trans e
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG (Filtration.submodule F)
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
⊢ (∃ n₀,
      Filtration.submodule F =
        Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n₀), (fun a => ↑(single R i) a) '' ↑(N F i))) →
    Submodule.FG (Filtration.submodule F)
rintro ⟨n, hn⟩
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i)))
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG (Filtration.submodule F)
rw [hn]
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG
    (⨆ (x : { i // i ∈ Finset.range (Nat.succ n) }),
      Submodule.span { x // x ∈ reesAlgebra I } ((fun a => ↑(single R ↑x) a) '' ↑(N F ↑x)))
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i)))
simp_rw [Submodule.span_iUnion₂, ← Finset.mem_range_succ_iff, iSup_subtype']
case mpr.intro.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ ∀ (i : { i // i ∈ Finset.range (Nat.succ n) }),
    Submodule.FG (Submodule.span { x // x ∈ reesAlgebra I } ((fun a => ↑(single R ↑i) a) '' ↑(N F ↑i)))
case mpr.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ Submodule.FG
    (⨆ (x : { i // i ∈ Finset.range (Nat.succ n) }),
      Submodule.span { x // x ∈ reesAlgebra I } ((fun a => ↑(single R ↑x) a) '' ↑(N F ↑x)))
apply Submodule.fg_iSup
case mpr.intro.h.mk
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
case mpr.intro.h
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
⊢ ∀ (i : { i // i ∈ Finset.range (Nat.succ n) }),
    Submodule.FG (Submodule.span { x // x ∈ reesAlgebra I } ((fun a => ↑(single R ↑i) a) '' ↑(N F ↑i)))
rintro ⟨i, hi⟩
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
case mpr.intro.h.mk
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
obtain ⟨s, hs⟩ := hF' i
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
this :
  Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
have : Submodule.span (reesAlgebra I) (s.image (lsingle R i) : Set (PolynomialModule R M)) =
    Submodule.span _ (single R i '' (F.N i : Set M)) := by
  rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]; rfl
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
this :
  Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
⊢ Submodule.FG (Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s))
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
this :
  Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
⊢ Submodule.FG
    (Submodule.span { x // x ∈ reesAlgebra I }
      ((fun a => ↑(single R ↑{ val := i, property := hi }) a) '' ↑(N F ↑{ val := i, property := hi })))
rw [Subtype.coe_mk, ← this]
no goals
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
this :
  Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
⊢ Submodule.FG (Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s))
exact ⟨_, rfl⟩
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
⊢ Submodule.span { x // x ∈ reesAlgebra I } ↑(Submodule.map (lsingle R i) (N F i)) =
    Submodule.span { x // x ∈ reesAlgebra 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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
⊢ Submodule.span { x // x ∈ reesAlgebra I } ↑(Finset.image (↑(lsingle R i)) s) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
rw [Finset.coe_image, ← Submodule.span_span_of_tower R, ← Submodule.map_span, hs]
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
hF' : ∀ (i : ℕ), Submodule.FG (N F i)
n : ℕ
hn :
  Filtration.submodule F =
    Submodule.span { x // x ∈ reesAlgebra I } (⋃ (i : ℕ) (_ : i ≤ n), (fun a => ↑(single R i) a) '' ↑(N F i))
i : ℕ
hi : i ∈ Finset.range (Nat.succ n)
s : Finset M
hs : Submodule.span R ↑s = N F i
⊢ Submodule.span { x // x ∈ reesAlgebra I } ↑(Submodule.map (lsingle R i) (N F i)) =
    Submodule.span { x // x ∈ reesAlgebra I } (↑(single R i) '' ↑(N F i))
rfl