-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
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
hα : α.IsNonZero
k : ℕ
h₁ :
  HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
h₂ : k ≤ chainLength α β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
mpr :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K) +
            (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
              (⇑β : (a : ↥H) → K))) ≠
        ⊥),
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₁ :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑k : ℤ) (⇑α : (a : ↥H) → K) +
            (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
              (⇑β : (a : ↥H) → K))) ≠
        ⊥),
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₂ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑k : ℤ)) (⇑α : (a : ↥H) → K) +
            (HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
              (⇑β : (a : ↥H) → K))) ≠
        ⊥),
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₃ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑k : ℤ)) (⇑α : (a : ↥H) → K) +
              HSMul.hSMul (α := ℤ) (β := ↥H → K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K)) ≠
        ⊥),
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
mpr₄ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (β := (a : ↥H) → K) (HAdd.hAdd (α := ℤ) (-(↑k : ℤ)) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K)) ≠
        ⊥),
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
have mpr₅ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) ≠
      ⊥),
  rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑k : ℤ))
          (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
Tactic: rwa [coe_chainTop, ← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul,
      ← add_assoc, ← add_smul, ← sub_eq_neg_add] at this
Cleared hypotheses: this