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
h : ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
n : ℕ
hn : n ≥ Exists.choose h
⊢ I • N F n = N F (n + 1)
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
⊢ Stable F ↔ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
refine' ⟨Stable.exists_pow_smul_eq_of_ge, fun h => ⟨h.choose, fun n hn => _⟩⟩
no goals
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
h : ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
n : ℕ
hn : n ≥ Exists.choose h
⊢ I • N F n = N F (n + 1)
rw [h.choose_spec n hn, h.choose_spec (n + 1) (by linarith), smul_smul, ← pow_succ,
  tsub_add_eq_add_tsub hn]
no goals
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
h : ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
n : ℕ
hn : n ≥ Exists.choose h
⊢ n + 1 ≥ Exists.choose h
linarith