-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Linear (goal)
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 χ) ⊥
x y : L
rw : finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) = finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • (χ x + χ y)
rw₁ :
  finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ (x + y) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₂ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₃ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x + finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ y
rw₄ :
  (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) (x + y) =
    (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) x + (finrank.{u_2, u_4} R ↥(genWeightSpace M χ) • χ) y
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)
      (x + y) =
    HAdd.hAdd (α := R) (β := R)
      (((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)
      (((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)
          y :
        R)
⊢ χ (x + y) = χ x + χ y
have rw₆ : HAdd.hAdd (α := R) (β := R)
    (((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)
    (((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)
        y :
      R) =
  HAdd.hAdd (α := R) (β := R)
    (((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)
    (((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)
        y :
      R)
Tactic: rw [← smul_right_inj (zero_lt_finrank_genWeightSpace hχ).ne', smul_add, ← Pi.smul_apply,
      ← Pi.smul_apply, ← Pi.smul_apply, ← trace_comp_toEnd_genWeightSpace_eq, map_add]