-- Mathlib/RingTheory/Filtration.lean
theorem Stable.of_le [IsNoetherianRing R] [Module.Finite R M] (hF : F.Stable)
    {F' : I.Filtration M} (hf : F' ≤ F) : F'.Stable

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : ∀ s ≤ F.submodule, s.FG
⊢ F'.submodule.FG

Tactic:
exact this _ (OrderHomClass.mono (submoduleInfHom M I) hf)

Result:
no goals

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : IsNoetherian ↥(reesAlgebra I) ↥F.submodule
⊢ F'.submodule.FG

Tactic:
rw [isNoetherian_submodule] at this

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : ∀ s ≤ F.submodule, s.FG
⊢ F'.submodule.FG

Proof state:
case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
i : ℕ
⊢ (F.N i).FG

Tactic:
exact IsNoetherian.noetherian _

Result:
no goals

Proof state:
case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F.N i).FG

Tactic:
intro i

Result:
case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.Stable

Tactic:
rw [← submodule_fg_iff_stable] at hF ⊢

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F'.N i).FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

Tactic:
have := isNoetherian_of_fg_of_noetherian _ hF

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
this : IsNoetherian ↥(reesAlgebra I) ↥F.submodule
⊢ F'.submodule.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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F'.N i).FG

case hF'
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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.Stable
F' : I.Filtration M
hf : F' ≤ F
⊢ ∀ (i : ℕ), (F.N i).FG

Tactic:
any_goals intro i; exact IsNoetherian.noetherian _

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
inst✝¹ : IsNoetherianRing R
inst✝ : Module.Finite R M
hF : F.submodule.FG
F' : I.Filtration M
hf : F' ≤ F
⊢ F'.submodule.FG