case intro
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ ∃ n₀, ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
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
⊢ ∃ n₀, ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
obtain ⟨n₀, hn⟩ := 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
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F 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
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ ∃ n₀, ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
use 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
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
k : ℕ
⊢ N F (n₀ + k) = I ^ k • N F 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
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
intro k
case intro.zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ N F (n₀ + Nat.zero) = I ^ Nat.zero • N F n₀

case intro.succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
n✝ : ℕ
ih : N F (n₀ + n✝) = I ^ n✝ • N F n₀
⊢ N F (n₀ + Nat.succ n✝) = I ^ Nat.succ n✝ • N F 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
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
k : ℕ
⊢ N F (n₀ + k) = I ^ k • N F n₀
induction' k with _ ih
no goals
case intro.zero
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
⊢ N F (n₀ + Nat.zero) = I ^ Nat.zero • N F n₀
simp
case intro.succ.a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
n✝ : ℕ
ih : N F (n₀ + n✝) = I ^ n✝ • N F n₀
⊢ n₀ + n✝ ≥ n₀
case intro.succ
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
n✝ : ℕ
ih : N F (n₀ + n✝) = I ^ n✝ • N F n₀
⊢ N F (n₀ + Nat.succ n✝) = I ^ Nat.succ n✝ • N F n₀
rw [Nat.succ_eq_add_one, ← add_assoc, ← hn, ih, add_comm, pow_add, mul_smul, pow_one]
no goals
case intro.succ.a
R M : Type u
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F F' : Filtration I M
n₀ : ℕ
hn : ∀ (n : ℕ), n ≥ n₀ → I • N F n = N F (n + 1)
n✝ : ℕ
ih : N F (n₀ + n✝) = I ^ n✝ • N F n₀
⊢ n₀ + n✝ ≥ n₀
linarith