-- Mathlib/Algebra/Lie/Weights/Linear.lean
lemma trace_comp_toEnd_genWeightSpace_eq (χ : L → R) :
    LinearMap.trace R _ ∘ₗ (toEnd R L (genWeightSpace M χ)).toLinearMap =
    finrank R (genWeightSpace M χ) • χ

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
have h₂ : LinearMap.trace R _ n = 0 := IsReduced.eq_zero _ <|
  LinearMap.isNilpotent_trace_of_isNilpotent <| isNilpotent_toEnd_sub_algebraMap M χ x

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
h₂ : (LinearMap.trace R ↥(genWeightSpace M χ)) n = 0
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
⊢ ⇑(LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) = finrank R ↥(genWeightSpace M χ) • χ

Tactic:
ext x

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
have h₁ : toEnd R L (genWeightSpace M χ) x = n + χ x • LinearMap.id := eq_add_of_sub_eq rfl

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
h₂ : (LinearMap.trace R ↥(genWeightSpace M χ)) n = 0
⊢ 0 + (LinearMap.trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id) = (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
simp [mul_comm (χ x)]

Result:
no goals

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
let n := toEnd R L (genWeightSpace M χ) x - χ x • LinearMap.id

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Proof state:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
h₂ : (LinearMap.trace R ↥(genWeightSpace M χ)) n = 0
⊢ (LinearMap.trace R ↥(genWeightSpace M χ) ∘ₗ ↑(toEnd R L ↥(genWeightSpace M χ))) x =
    (finrank R ↥(genWeightSpace M χ) • χ) x

Tactic:
rw [LinearMap.comp_apply, LieHom.coe_toLinearMap, h₁, map_add, h₂]

Result:
case h
R : Type u_2
L : Type u_3
M : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra R L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : LieModule R L M
inst✝⁴ : IsDomain R
inst✝³ : IsPrincipalIdealRing R
inst✝² : Free R M
inst✝¹ : Module.Finite R M
inst✝ : LieRing.IsNilpotent L
χ : L → R
x : L
n : End R ↥(genWeightSpace M χ) := (toEnd R L ↥(genWeightSpace M χ)) x - χ x • LinearMap.id
h₁ : (toEnd R L ↥(genWeightSpace M χ)) x = n + χ x • LinearMap.id
h₂ : (LinearMap.trace R ↥(genWeightSpace M χ)) n = 0
⊢ 0 + (LinearMap.trace R ↥(genWeightSpace M χ)) (χ x • LinearMap.id) = (finrank R ↥(genWeightSpace M χ) • χ) x