-- Module: Mathlib.Algebra.Lie.Weights.Linear
Goal:
k : Type u_1
R : Type u_2
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
inst_7 : IsDomain R
inst_8 : IsPrincipalIdealRing R
inst_9 : Free R M
inst_10 : Module.Finite R M
inst_11 : LieRing.IsNilpotent L
inst_12 : CharZero R
χ : L → R
hχ : Ne (α := LieSubmodule R L M) (genWeightSpace M χ) ⊥
t : R
x : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • t • χ x
rw₁ : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₂ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x
rw₃ : (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (t • x) = t • (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x
rw₄ :
  ((LinearMap.trace R ↥(genWeightSpace M χ) :
            LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
          ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
              LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
        (a : L) → R)
      (t • x) =
    HSMul.hSMul (β := R) t
      (((LinearMap.trace R ↥(genWeightSpace M χ) :
                LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
              ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            (a : L) → R)
          x :
        R)
rw₅ rw₆ :
  HSMul.hSMul (β := R) t
      (((LinearMap.trace R ↥(genWeightSpace M χ) :
                LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
              ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            (a : L) → R)
          x :
        R) =
    HSMul.hSMul (β := R) t
      (((LinearMap.trace R ↥(genWeightSpace M χ) :
                LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥(genWeightSpace M χ) →ₗ[R] ↥(genWeightSpace M χ)) R) ∘ₗ
              ((↑(toEnd.{u_2, u_3, u_4} R L ↥(genWeightSpace M χ)) :
                  LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
                LinearMap.{u_2, u_2, u_3, u_4} (RingHom.id R) L (End R ↥(genWeightSpace M χ))) :
            (a : L) → R)
          x :
        R)
⊢ χ (t • x) = t • χ x

Tactic:
rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_comm, ← Pi.smul_apply,
      ← Pi.smul_apply (finrank R _), ← trace_comp_toEnd_genWeightSpace_eq, map_smul]

Premises used: LieModule.trace_comp_toEnd_genWeightSpace_eq, LT.lt.ne', LieModule.zero_lt_finrank_genWeightSpace, SMulCommClass.smul_comm, smul_right_inj, Module.finrank, map_smul, Pi.smul_apply