-- Mathlib/RingTheory/Finiteness/Nilpotent.lean
theorem Module.End.isNilpotent_iff_of_finite [Module.Finite R M] {f : End R M} :
    IsNilpotent f ↔ ∀ m : M, ∃ n : ℕ, (f ^ n) m = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ n, (f ^ n) m = 0
⊢ IsNilpotent f

Tactic:
rcases Module.Finite.fg_top (R := R) (M := M) with ⟨S, hS⟩

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ n, (f ^ n) m = 0
S : Finset M
hS : Submodule.span R ↑S = ⊤
⊢ IsNilpotent f

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
x✝ : IsNilpotent f
m : M
n : ℕ
hn : f ^ n = 0
⊢ (f ^ n) m = 0

Tactic:
simp [hn]

Result:
no goals

Proof state:
case h.h.add
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m x✝ y✝ : M
hx✝ : x✝ ∈ Submodule.span R ↑S
hy✝ : y✝ ∈ Submodule.span R ↑S
a✝¹ : (f ^ S.sup g) x✝ = 0 x✝
a✝ : (f ^ S.sup g) y✝ = 0 y✝
⊢ (f ^ S.sup g) (x✝ + y✝) = 0 (x✝ + y✝)

Tactic:
simp_all

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ n, (f ^ n) m = 0
S : Finset M
hS : Submodule.span R ↑S = ⊤
⊢ IsNilpotent f

Tactic:
choose g hg using h

Result:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
⊢ IsNilpotent f

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ (f ^ S.sup g) m = 0 m

Tactic:
have hm : m ∈ Submodule.span R S := by simp [hS]

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
hm : m ∈ Submodule.span R ↑S
⊢ (f ^ S.sup g) m = 0 m

Proof state:
case h.h.mem
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m x : M
hx : x ∈ ↑S
⊢ (f ^ S.sup g) x = 0 x

Tactic:
exact LinearMap.pow_map_zero_of_le (Finset.le_sup hx) (hg x)

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
⊢ f ^ S.sup g = 0

Tactic:
ext m

Result:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ (f ^ S.sup g) m = 0 m

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
⊢ IsNilpotent f ↔ ∀ (m : M), ∃ n, (f ^ n) m = 0

Tactic:
refine ⟨fun ⟨n, hn⟩ m ↦ ⟨n, by simp [hn]⟩, fun h ↦ ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
h : ∀ (m : M), ∃ n, (f ^ n) m = 0
⊢ IsNilpotent f

Proof state:
case h.h.zero
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ (f ^ S.sup g) 0 = 0 0

Tactic:
simp

Result:
no goals

Proof state:
case h.h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
hm : m ∈ Submodule.span R ↑S
⊢ (f ^ S.sup g) m = 0 m

Tactic:
induction hm using Submodule.span_induction with
| mem x hx => exact LinearMap.pow_map_zero_of_le (Finset.le_sup hx) (hg x)
| zero => simp
| add => simp_all
| smul => simp_all

Result:
no goals

Proof state:
case h.h.smul
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
a✝¹ : R
x✝ : M
hx✝ : x✝ ∈ Submodule.span R ↑S
a✝ : (f ^ S.sup g) x✝ = 0 x✝
⊢ (f ^ S.sup g) (a✝¹ • x✝) = 0 (a✝¹ • x✝)

Tactic:
simp_all

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
⊢ IsNilpotent f

Tactic:
use Finset.sup S g

Result:
case h
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
⊢ f ^ S.sup g = 0

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
f : End R M
S : Finset M
hS : Submodule.span R ↑S = ⊤
g : M → ℕ
hg : ∀ (m : M), (f ^ g m) m = 0
m : M
⊢ m ∈ Submodule.span R ↑S

Tactic:
simp [hS]

Result:
no goals