-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
h :
  -(⇑α : (a : ↥H) → K) =
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
        (-(⇑α : (a : ↥H) → K)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → K))
h₁ :
  -(⇑α : (a : ↥H) → K) =
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
        (-(⇑α : (a : ↥H) → K)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        0)
h₂ :
  -(⇑α : (a : ↥H) → K) =
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
        (-(⇑α : (a : ↥H) → K)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
h₃ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (-(⇑α : (a : ↥H) → K)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
h₄ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (-(⇑α : (a : ↥H) → K)) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K))
h₅ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
      (-HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
            (⇑α : (a : ↥H) → K) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K))
h₆ : -(⇑α : (a : ↥H) → K) = HAdd.hAdd (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) 0
h₇ h₈ : Eq (α := ↥H → K) (-(⇑α : (a : ↥H) → K)) (-(⇑α : (a : ↥H) → K))
⊢ -(⇑α : (a : ↥H) → K) =
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
        (-(⇑α : (a : ↥H) → K)) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)

Tactic:
rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]

Premises used: LieModule.Weight.coe_zero, add_assoc, smul_neg, neg_add_cancel, succ_nsmul', add_zero, LieModule.coe_chainTop'