-- 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
n : ℕ
hn : chainLength α β < n + chainTopCoeff (⇑α : (a : ↥H) → K) β
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (n + chainTopCoeff (⇑α : (a : ↥H) → K) β) (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
rwa :
  ∀
    (this :
      rootSpace H
          (-HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
                (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₁ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₂ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → 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) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₃ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → 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) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₄ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (β := (a : ↥H) → K)
              (HAdd.hAdd (α := ℤ) (-(↑(n + chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
                (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
rwa₅ :
  ∀
    (this :
      rootSpace H
          (HSMul.hSMul (β := (a : ↥H) → K)
              (-HAdd.hAdd (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) +
                (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
              (⇑α : (a : ↥H) → K) +
            (⇑β : (a : ↥H) → K)) =
        ⊥),
    rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
have rwa₆ : ∀
  (this :
    rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K)
            (HAdd.hAdd (α := ℤ) (-(↑n : ℤ)) (-(↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) +
              (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
            (⇑α : (a : ↥H) → K) +
          (⇑β : (a : ↥H) → K)) =
      ⊥),
  rootSpace H (HSMul.hSMul (α := ℤ) (β := (a : ↥H) → K) (-(↑n : ℤ)) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)) = ⊥
Tactic: rwa [← Nat.cast_smul_eq_nsmul ℤ, ← neg_smul, coe_chainTop, ← add_assoc,
    ← add_smul, Nat.cast_add, neg_add, add_assoc, neg_add_cancel, add_zero] at this
Cleared hypotheses: this