-- 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
n : ℤ
hβ' : (⇑β' : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
hα : ¬α.IsZero
neg :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainLength α β) : ℤ)
neg₁ :
  Eq (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β' + chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ)
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₂ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β + chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₃ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β') : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₄ :
  (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n + (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₅ :
  (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n + ((↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₆ :
  (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + -n + ((↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₇ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) +
      (-n + n) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₈ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + 0 =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
neg₉ neg₁₀ :
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) =
    HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)

Tactic:
rw [← chainTopCoeff_add_chainBotCoeff, ← chainTopCoeff_add_chainBotCoeff,
      Nat.cast_add, Nat.cast_add, chainTopCoeff_of_eq_zsmul_add α β hα β' n hβ',
      chainBotCoeff_of_eq_zsmul_add α β hα β' n hβ', sub_eq_add_neg, add_add_add_comm,
      neg_add_cancel, add_zero]

Premises used: sub_eq_add_neg, Nat.cast_add, LieAlgebra.IsKilling.chainTopCoeff_add_chainBotCoeff, neg_add_cancel, LieAlgebra.IsKilling.chainBotCoeff_of_eq_zsmul_add, add_add_add_comm, LieAlgebra.IsKilling.chainTopCoeff_of_eq_zsmul_add, add_zero