awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₄ : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n + (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β') : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₅ : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) - n + ((↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₆ : (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + -n + ((↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + n) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₇ : HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) +
    (-n + n) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₈ : HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) + 0 =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
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) β) : ℤ)
⊢ Eq (α := ℤ) (↑(chainLength α β') : ℤ) (↑(chainLength α β) : ℤ)
have neg₉ : HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
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]
-- 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
inst_8 : Nontrivial L
hα : α.IsNonZero
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 = 1
have symm : 1 = chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: symm
-- 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
inst_8 : Nontrivial L
hα : α.IsNonZero
⊢ 1 = chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have h₁ : 1 ≤ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: apply eq_of_le_of_not_lt
-- 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
inst_8 : Nontrivial L
hα : α.IsNonZero
h₁ : 1 ≤ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ 1 = chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have h₂ : ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: apply eq_of_le_of_not_lt
-- 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
inst_8 : Nontrivial L
hα : α.IsNonZero
⊢ 1 ≤ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have h₁ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 ≠ 0
Tactic: rw [Nat.one_le_iff_ne_zero]
-- 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
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
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have h₂ : ∀ (h e f : L) (isSl2 : IsSl2Triple h e f) (he : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
  (hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
  ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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
h e f : L
isSl2 : IsSl2Triple h e f
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have isSl2₁ : IsSl2Triple (↑(coroot α) : L) e f
Tactic: obtain rfl := isSl2.h_eq_coroot hα he hf
Cleared hypotheses: h, isSl2
-- 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
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
this :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := ↥H → K) (⇑α : (a : ↥H) → K) (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)))
    ⁅e, x⁆
⊢ ⁅e, x⁆ = 0
have rwa : ∀ (this : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅e, x⁆), ⁅e, x⁆ = 0
Tactic: rwa [genWeightSpace_add_chainTop _ _ hα] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
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
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
Tactic: have prim : isSl2.HasPrimitiveVectorWith x (chainLength α (0 : Weight K H L) : K) :=
    have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
    ⟨x_ne0, (chainLength_smul _ _ hx).symm, by rwa [genWeightSpace_add_chainTop _ _ hα] at this⟩
-- 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
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)
⊢ Membership.mem (α := L) (rootSpace H (-(⇑α : (a : ↥H) → K)))
    ((HPow.hPow (α := End K L) ((toEnd K L L : (a : L) → End K L) f : End K L)
            (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1) :
          (a : L) → L)
        x :
      L)
have 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)) +
    (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)
Tactic: convert! toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2
-- 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
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)
⊢ -(⇑α : (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)
have 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))
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]