-- Mathlib/RingTheory/Filtration.lean
theorem submodule_eq_span_le_iff_stable_ge (n₀ : ℕ) :
    F.submodule = Submodule.span _ (⋃ i ≤ n₀, single R i '' (F.N i : Set M)) ↔
      ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Proof state:
case neg.intro.intro.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : ⇑(single R j) '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
x y : M
hx : (single R (j + 1)) x ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hy : (single R (j + 1)) y ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
⊢ (single R (j + 1)) (x + y) ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))

Tactic:
rw [map_add]

Result:
case neg.intro.intro.refine_2
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : ⇑(single R j) '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
x y : M
hx : (single R (j + 1)) x ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hy : (single R (j + 1)) y ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
⊢ (single R (j + 1)) x + (single R (j + 1)) y ∈
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
i : ℕ
⊢ ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'

Tactic:
intro i hi

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
i✝ i : ℕ
hi : i ≤ n₀
⊢ ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : ⇑(single R j) '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hj' : j.succ ≤ n₀
⊢ ⇑(single R (j + 1)) '' ↑(F.N (j + 1)) ⊆
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))

Tactic:
exact this _ hj'

Result:
no goals

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : ⇑(single R j) '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hj' : n₀ ≤ j
⊢ ⇑(single R (j + 1)) '' ↑(I • F.N j) ⊆
    ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))

Tactic:
rintro _ ⟨m, hm, rfl⟩

Result:
case neg.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
F' : Submodule (↥(reesAlgebra I)) (PolynomialModule R M) :=
  Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))
hF : ∀ n ≥ n₀, I • F.N n = F.N (n + 1)
this : ∀ i ≤ n₀, ⇑(single R i) '' ↑(F.N i) ⊆ ↑F'
j : ℕ
hj : ⇑(single R j) '' ↑(F.N j) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
hj' : n₀ ≤ j
m : M
hm : m ∈ ↑(I • F.N j)
⊢ (single R (j + 1)) m ∈ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ⇑(single R i) '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l) (n + 1) = x
⊢ ∀ c ∈ l.support, (fun a₁ b => (b • ↑a₁) (n + 1)) c (l c) ∈ I • F.N n

Tactic:
rintro ⟨_, _, ⟨n', rfl⟩, _, ⟨hn', rfl⟩, m, hm, rfl⟩ -

Result:
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ⇑(single R i) '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l) (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
⊢ (fun a₁ b => (b • ↑a₁) (n + 1)) ⟨(single R n') m, ⋯⟩ (l ⟨(single R n') m, ⋯⟩) ∈ I • F.N n

Proof state:
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ⇑(single R i) '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l) (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
⊢ (↑(l ⟨(single R n') m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n

Tactic:
have := F.pow_smul_le_pow_smul (n - n') n' 1

Result:
case mk.intro.intro.intro.intro.intro.intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
n₀ : ℕ
H :
  ∀ (i : ℕ),
    ⇑(single R i) '' ↑(F.N i) ⊆ ↑(Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)))
n : ℕ
hn : n ≥ n₀
x : M
hx : x ∈ F.N (n + 1)
l : ↑(⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i)) →₀ ↥(reesAlgebra I)
hl : ((Finsupp.linearCombination (↥(reesAlgebra I)) Subtype.val) l) (n + 1) = x
n' : ℕ
hn' : n' ≤ n₀
m : M
hm : m ∈ ↑(F.N n')
e : n' ≤ n
this : I ^ (n - n' + 1) • F.N n' ≤ I ^ 1 • F.N (n - n' + n')
⊢ (↑(l ⟨(single R n') m, ⋯⟩)).coeff (n + 1 - n') • m ∈ I • F.N n