-- Mathlib/LinearAlgebra/Trace.lean
lemma isNilpotent_trace_of_isNilpotent {f : M →ₗ[R] M} (hf : IsNilpotent f) :
    IsNilpotent (trace R M f)

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
⊢ IsNilpotent ((trace R M) f)

Tactic:
by_cases H : ∃ s : Finset M, Nonempty (Basis s R M)

Result:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

Tactic:
rw [LinearMap.trace, dif_neg H]

Result:
case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent (0 f)

Proof state:
case pos.intro.intro.hM
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((toMatrix b b) f)

Tactic:
simpa

Result:
no goals

Proof state:
case pos.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((trace R M) f)

Tactic:
classical
rw [trace_eq_matrix_trace R b]
apply Matrix.isNilpotent_trace_of_isNilpotent
simpa

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent (0 f)

Tactic:
exact IsNilpotent.zero

Result:
no goals

Proof state:
case pos.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((trace R M) f)

Tactic:
rw [trace_eq_matrix_trace R b]

Result:
case pos.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((toMatrix b b) f).trace

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

Tactic:
swap

Result:
case neg
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ¬∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

Proof state:
case pos
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
H : ∃ s, Nonempty (Basis { x // x ∈ s } R M)
⊢ IsNilpotent ((trace R M) f)

Tactic:
obtain ⟨s, ⟨b⟩⟩ := H

Result:
case pos.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((trace R M) f)

Proof state:
case pos.intro.intro
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((toMatrix b b) f).trace

Tactic:
apply Matrix.isNilpotent_trace_of_isNilpotent

Result:
case pos.intro.intro.hM
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : M →ₗ[R] M
hf : IsNilpotent f
s : Finset M
b : Basis { x // x ∈ s } R M
⊢ IsNilpotent ((toMatrix b b) f)