case h.e'_2.h.e'_4.h
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
inst✝ : LocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ 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
inst✝ : LocalRing R
h : I ≠ ⊤
⊢ (⨅ (i : ℕ), I ^ i) = ⊥
convert I.iInf_pow_smul_eq_bot_of_localRing (M := R) h
case h.e'_2.h.e'_4.h.h
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
inst✝ : LocalRing R
h : I ≠ ⊤
x✝ : ℕ
i : R
⊢ i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤
case h.e'_2.h.e'_4.h
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
inst✝ : LocalRing R
h : I ≠ ⊤
x✝ : ℕ
⊢ I ^ x✝ = I ^ x✝ • ⊤
ext i
no goals
case h.e'_2.h.e'_4.h.h
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
inst✝ : LocalRing R
h : I ≠ ⊤
x✝ : ℕ
i : R
⊢ i ∈ I ^ x✝ ↔ i ∈ I ^ x✝ • ⊤
rw [smul_eq_mul, ← Ideal.one_eq_top, mul_one]