-- Mathlib/RingTheory/Filtration.lean
theorem submodule_fg_iff_stable (hF' : ∀ i, (F.N i).FG) : F.submodule.FG ↔ F.Stable

Proof state:
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), ⇑(single R i) '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (⇑(single R i) '' ↑(F.N i))
⊢ (Submodule.span (↥(reesAlgebra I)) (⇑(single R ↑⟨i, hi⟩) '' ↑(F.N ↑⟨i, hi⟩))).FG

Tactic:
rw [Subtype.coe_mk, ← this]

Result:
case mpr.intro.h.mk.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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), ⇑(single R i) '' ↑(F.N i))
i : ℕ
hi : i ∈ Finset.range n.succ
s : Finset M
hs : Submodule.span R ↑s = F.N i
this :
  Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s) =
    Submodule.span (↥(reesAlgebra I)) (⇑(single R i) '' ↑(F.N i))
⊢ (Submodule.span ↥(reesAlgebra I) ↑(Finset.image (⇑(lsingle R i)) s)).FG

Proof state:
case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ⇑(single R i) '' ↑(F.N i) ⊆ ⋃ i, ⋃ (_ : i ≤ m), ⇑(single R i) '' ↑(F.N i)

Tactic:
refine @Set.subset_iUnion₂ _ _ _ (fun i => fun _ => ↑((single R i) '' ((N F i) : Set M))) i ?_

Result:
case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ i ≤ m

Proof state:
case mpr.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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), ⇑(single R i) '' ↑(F.N i))
⊢ (⨆ x, Submodule.span (↥(reesAlgebra I)) (⇑(single R ↑x) '' ↑(F.N ↑x))).FG

Tactic:
apply Submodule.fg_iSup

Result:
case mpr.intro.h
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
hF' : ∀ (i : ℕ), (F.N i).FG
n : ℕ
hn : F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n), ⇑(single R i) '' ↑(F.N i))
⊢ ∀ (i : Subtype (Membership.mem (Finset.range n.succ))),
    (Submodule.span (↥(reesAlgebra I)) (⇑(single R ↑i) '' ↑(F.N ↑i))).FG

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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ F.Stable

Tactic:
delta Ideal.Filtration.Stable

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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG ↔ ∃ n₀, ∀ n ≥ n₀, I • F.N n = F.N (n + 1)

Proof state:
case mp.refine_2.e_s.h.mp.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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
i : ℕ
e : ∃ x ∈ F.N i, (single R i) x = x✝
⊢ ∃ i, ∃ x ∈ F.N i, (single R i) x = x✝

Tactic:
exact ⟨i, e⟩

Result:
no goals

Proof state:
case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
⊢ ∀ i ≤ n,
    ⇑(single R i) '' ↑(F.N i) ⊆
      ↑((fun n₀ => Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))) m)

Tactic:
intro i hi

Result:
case mp.refine_1
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
n m : ℕ
e : n ≤ m
i : ℕ
hi : i ≤ n
⊢ ⇑(single R i) '' ↑(F.N i) ⊆
    ↑((fun n₀ => Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))) m)

Proof state:
case mp.refine_2.e_s
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ≤ i), ⇑(single R i_1) '' ↑(F.N i_1) = ⋃ i, ⇑(single R i) '' ↑(F.N i)

Tactic:
ext

Result:
case mp.refine_2.e_s.h
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ x✝ ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ≤ i), ⇑(single R i_1) '' ↑(F.N i_1) ↔ x✝ ∈ ⋃ i, ⇑(single R i) '' ↑(F.N i)

Proof state:
case mp.refine_2.e_s.h
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ x✝ ∈ ⋃ i, ⋃ i_1, ⋃ (_ : i_1 ≤ i), ⇑(single R i_1) '' ↑(F.N i_1) ↔ x✝ ∈ ⋃ i, ⇑(single R i) '' ↑(F.N i)

Tactic:
simp only [Set.mem_iUnion, Set.mem_image, SetLike.mem_coe, exists_prop]

Result:
case mp.refine_2.e_s.h
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ (∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝) ↔ ∃ i, ∃ x ∈ F.N i, (single R i) x = x✝

Proof state:
case mp
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
hF' : ∀ (i : ℕ), (F.N i).FG
⊢ F.submodule.FG →
    ∃ n₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))

Tactic:
rintro H

Result:
case mp
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
⊢ ∃ n₀, F.submodule = Submodule.span (↥(reesAlgebra I)) (⋃ i, ⋃ (_ : i ≤ n₀), ⇑(single R i) '' ↑(F.N i))

Proof state:
case mp.refine_2.e_s.h
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ (∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝) ↔ ∃ i, ∃ x ∈ F.N i, (single R i) x = x✝

Tactic:
constructor

Result:
case mp.refine_2.e_s.h.mp
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ (∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝) → ∃ i, ∃ x ∈ F.N i, (single R i) x = x✝

case mp.refine_2.e_s.h.mpr
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
hF' : ∀ (i : ℕ), (F.N i).FG
H : F.submodule.FG
x✝ : PolynomialModule R M
⊢ (∃ i, ∃ x ∈ F.N i, (single R i) x = x✝) → ∃ i, ∃ i_1 ≤ i, ∃ x ∈ F.N i_1, (single R i_1) x = x✝