case intro
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₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • 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₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq
case intro
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₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
⊢ ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - 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
h : Stable F
n₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
⊢ ∃ n₀, ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • 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
h : Stable F
n₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
n : ℕ
hn : n ≥ n₀
⊢ N F n = I ^ (n - 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
h : Stable F
n₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
⊢ ∀ (n : ℕ), n ≥ n₀ → N F n = I ^ (n - n₀) • N F n₀
intro n hn
case h.e'_2.h.e'_8
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₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - 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
h : Stable F
n₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
n : ℕ
hn : n ≥ n₀
⊢ N F n = I ^ (n - n₀) • N F n₀
convert hn₀ (n - n₀)
no goals
case h.e'_2.h.e'_8
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₀ : ℕ
hn₀ : ∀ (k : ℕ), N F (n₀ + k) = I ^ k • N F n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - n₀)
rw [add_comm, tsub_add_cancel_of_le hn]