-- Mathlib/LinearAlgebra/Trace.lean
lemma trace_comp_eq_mul_of_commute_of_isNilpotent [IsReduced R] {f g : Module.End R M}
    (μ : R) (h_comm : Commute f g) (hg : IsNilpotent (g - algebraMap R _ μ)) :
    trace R M (f ∘ₗ g) = μ * trace R M f

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ Commute f n

Tactic:
exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
replace hg : trace R M (f ∘ₗ n) = 0 := by
  rw [← isNilpotent_iff_eq_zero, ← mul_eq_comp]
  refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_right ?_ hg)
  exact h_comm.sub_right (Algebra.commute_algebraMap_right μ f)

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
have hμ : g = algebraMap R _ μ + n := eq_add_of_sub_eq' rfl

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ IsNilpotent ((trace R M) (f * n))

Tactic:
refine isNilpotent_trace_of_isNilpotent (Commute.isNilpotent_mul_right ?_ hg)

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ Commute f n

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
⊢ f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f

Tactic:
ext

Result:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
x✝ : M
⊢ (f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ) x✝ = (μ • f) x✝

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
hg : IsNilpotent (g - (algebraMap R (End R M)) μ)
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
set n := g - algebraMap R _ μ

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Proof state:
case h
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
x✝ : M
⊢ (f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ) x✝ = (μ • f) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ (trace R M) (f ∘ₗ n) = 0

Tactic:
rw [← isNilpotent_iff_eq_zero, ← mul_eq_comp]

Result:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : IsNilpotent n
⊢ IsNilpotent ((trace R M) (f * n))

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ g) = μ * (trace R M) f

Tactic:
rw [hμ, comp_add, map_add, hg, add_zero, this, LinearMap.map_smul, smul_eq_mul]

Result:
no goals