-- Mathlib/RingTheory/Filtration.lean
theorem Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors
    [IsNoetherianRing R] [NoZeroSMulDivisors R M]
    [Module.Finite R M] (h : I ≠ ⊤) : (⨅ i : ℕ, I ^ i • ⊤ : Submodule R M) = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
⊢ x ∈ ⊥

Tactic:
by_contra hx'

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
⊢ False

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this✝ : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
this : ↑r = 1
⊢ False

Tactic:
exact I.eq_top_iff_one.not.mp h (this ▸ r.prop)

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
⊢ False

Tactic:
have := smul_left_injective _ hx' (hr.trans (one_smul _ x).symm)

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this✝ : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
this : ↑r = 1
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ = ⊥

Tactic:
rw [eq_bot_iff]

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ ≤ ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
⊢ ⨅ i, I ^ i • ⊤ ≤ ⊥

Tactic:
intro x hx

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
⊢ x ∈ ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
⊢ False

Tactic:
have := Ideal.mem_iInf_smul_pow_eq_bot_iff I x

Result:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
⊢ False

Proof state:
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
⊢ False

Tactic:
obtain ⟨r, hr⟩ := this.mp hx

Result:
case intro
R : Type u_1
M : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
I : Ideal R
inst✝² : IsNoetherianRing R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : Module.Finite R M
h : I ≠ ⊤
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
hx' : x ∉ ⊥
this : x ∈ ⨅ i, I ^ i • ⊤ ↔ ∃ r, ↑r • x = x
r : ↥I
hr : ↑r • x = x
⊢ False