R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
let N := (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M)
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
have hN : ∀ k, (I.stableFiltration ⊤ ⊓ I.trivialFiltration N).N k = N :=
  fun k => inf_eq_right.mpr ((iInf_le _ k).trans <| le_of_eq <| by simp)
case mp
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x

case mpr
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ (i : ℕ), I ^ i • ⊤
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) ↔ ∃ r, ↑r • x = x
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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
k : ℕ
⊢ I ^ k • ⊤ = Filtration.N (stableFiltration I ⊤) k
simp
case mp
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x
case mp
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x
haveI := isNoetherian_of_fg_of_noetherian' hM.out
case mp.intro.intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
r : R
hr₁ : r ∈ I
hr₂ : ∀ (n : M), n ∈ N → r • n = n
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x
case mp
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x
obtain ⟨r, hr₁, hr₂⟩ :=
  Submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I N (IsNoetherian.noetherian N) (by
    obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
    have := hk k (le_refl _)
    rw [hN, hN] at this
    exact le_of_eq this.symm)
case mp.intro.intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
r : R
hr₁ : r ∈ I
hr₂ : ∀ (n : M), n ∈ N → r • n = n
H : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
⊢ ∃ r, ↑r • x = x
case mp.intro.intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
r : R
hr₁ : r ∈ I
hr₂ : ∀ (n : M), n ∈ N → r • n = n
⊢ (x ∈ ⨅ (i : ℕ), I ^ i • ⊤) → ∃ r, ↑r • x = x
intro H
no goals
case mp.intro.intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
r : R
hr₁ : r ∈ I
hr₂ : ∀ (n : M), n ∈ N → r • n = n
H : x ∈ ⨅ (i : ℕ), I ^ i • ⊤
⊢ ∃ r, ↑r • x = x
exact ⟨⟨r, hr₁⟩, hr₂ _ H⟩
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
⊢ 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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
⊢ N ≤ I • N
obtain ⟨k, hk⟩ := (I.stableFiltration_stable ⊤).inter_right (I.trivialFiltration N)
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this✝ : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
this :
  I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k =
    Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (k + 1)
⊢ N ≤ I • N
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
⊢ N ≤ I • N
have := hk k (le_refl _)
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this✝ : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
this : I • N = N
⊢ N ≤ I • N
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this✝ : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
this :
  I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k =
    Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (k + 1)
⊢ N ≤ I • N
rw [hN, hN] at this
no goals
case intro
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
this✝ : IsNoetherian R M
k : ℕ
hk :
  ∀ (n : ℕ),
    n ≥ k →
      I • Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) n =
        Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) (n + 1)
this : I • N = N
⊢ N ≤ I • N
exact le_of_eq this.symm
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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ x ∈ ⨅ (i : ℕ), I ^ 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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
⊢ (∃ r, ↑r • x = x) → x ∈ ⨅ (i : ℕ), I ^ i • ⊤
rintro ⟨r, eq⟩
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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ ∀ (i : ℕ), x ∈ I ^ 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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ x ∈ ⨅ (i : ℕ), I ^ i • ⊤
rw [Submodule.mem_iInf]
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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
⊢ x ∈ I ^ 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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ ∀ (i : ℕ), x ∈ I ^ i • ⊤
intro i
case mpr.intro.zero
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ x ∈ I ^ Nat.zero • ⊤

case mpr.intro.succ
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ Nat.succ 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
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
⊢ x ∈ I ^ i • ⊤
induction' i with i hi
no goals
case mpr.intro.zero
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
⊢ x ∈ I ^ Nat.zero • ⊤
simp
case mpr.intro.succ
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ ↑r • x ∈ I • I ^ i • ⊤
case mpr.intro.succ
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ x ∈ I ^ Nat.succ i • ⊤
rw [Nat.succ_eq_one_add, pow_add, ← smul_smul, pow_one, ← eq]
no goals
case mpr.intro.succ
R M : Type u
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
I : Ideal R
F F' : Filtration I M
inst✝ : IsNoetherianRing R
hM : Module.Finite R M
x : M
N : Submodule R M := ⨅ (i : ℕ), I ^ i • ⊤
hN : ∀ (k : ℕ), Filtration.N (stableFiltration I ⊤ ⊓ trivialFiltration I N) k = N
r : { x // x ∈ I }
eq : ↑r • x = x
i : ℕ
hi : x ∈ I ^ i • ⊤
⊢ ↑r • x ∈ I • I ^ i • ⊤
exact Submodule.smul_mem_smul r.prop hi