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

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ (1 - ↑r) • x = (1 - ↑r) • 0

Tactic:
simp [sub_smul, hr]

Result:
no goals

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ 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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ 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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
⊢ x ∈ ⊥

Tactic:
obtain ⟨r, hr⟩ := (I.mem_iInf_smul_pow_eq_bot_iff x).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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
⊢ 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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
⊢ ⨅ 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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
⊢ 1 - ↑r - 1 ∈ ⊥.jacobson

Tactic:
simpa using h r.2

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ x ∈ ⊥

Tactic:
apply this.smul_left_cancel.mp

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ (1 - ↑r) • x = (1 - ↑r) • 0

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
⊢ x ∈ ⊥

Tactic:
have := isUnit_of_sub_one_mem_jacobson_bot (1 - r.1) (by simpa using h r.2)

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✝ : Module.Finite R M
h : I ≤ ⊥.jacobson
x : M
hx : x ∈ ⨅ i, I ^ i • ⊤
r : ↥I
hr : ↑r • x = x
this : IsUnit (1 - ↑r)
⊢ x ∈ ⊥