awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
this :
  Eq.{u_1 + 1} (α := K) ((W : (a : ↥H) → K) (coroot (-α)) : K)
    ((↑((↑(chainLength (-α) W) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) : ℤ)) : K) : K)
⊢ 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
have this₁ : chainTopCoeff (⇑(-α) : (a : ↥H) → K) W + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W + (n + n) =
  chainLength (-α) W + chainLength α β
Tactic: simp only [coroot_neg, map_neg, hW, nsmul_eq_mul, Pi.natCast_def, coe_chainTop, zsmul_eq_mul,
      Int.cast_natCast, Pi.add_apply, Pi.neg_apply, Pi.mul_apply, root_apply_coroot hα, mul_two,
      apply_coroot_eq_cast' α β, Int.cast_sub, Int.cast_mul, Int.cast_ofNat, mul_comm (2 : K),
      add_sub_cancel, add_sub, Nat.cast_inj, eq_sub_iff_add_eq, ← Nat.cast_add, ← sub_eq_neg_add,
      sub_eq_iff_eq_add] 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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ False
have H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
Tactic: have H₁ : 1 + n + chainTopCoeff (-α) W ≤ chainLength (-α) W := by
    have := apply_coroot_eq_cast' (-α) W
    simp only [coroot_neg, map_neg, hW, nsmul_eq_mul, Pi.natCast_def, coe_chainTop, zsmul_eq_mul,
      Int.cast_natCast, Pi.add_apply, Pi.neg_apply, Pi.mul_apply, root_apply_coroot hα, mul_two,
      apply_coroot_eq_cast' α β, Int.cast_sub, Int.cast_mul, Int.cast_ofNat, mul_comm (2 : K),
      add_sub_cancel, add_sub, Nat.cast_inj, eq_sub_iff_add_eq, ← Nat.cast_add, ← sub_eq_neg_add,
      sub_eq_iff_eq_add] at this
    lia
-- 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
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
⊢ HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K) =
    HSMul.hSMul (β := (a : ↥H) → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
have simp : HSMul.hSMul (β := (a : ↥H) → K)
      (HAdd.hAdd (α := ℤ) 1 (↑n : ℤ) + (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ) +
          HSub.hSub (α := ℤ) (-(↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ)) (↑n : ℤ) +
        (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
      (⇑α : (a : ↥H) → K) +
    (⇑β : (a : ↥H) → K) =
  HSMul.hSMul (β := (a : ↥H) → K) (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) 1)
      (⇑α : (a : ↥H) → K) +
    (⇑β : (a : ↥H) → K)
Tactic: simp only [Weight.coe_neg, ← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_add, Nat.cast_one, coe_chainTop,
      smul_neg, ← neg_smul, hW, ← add_assoc, ← add_smul, ← sub_eq_add_neg]
-- 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
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
⊢ HSMul.hSMul (β := (a : ↥H) → K)
        (HAdd.hAdd (α := ℤ) 1 (↑n : ℤ) + (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ) +
            HSub.hSub (α := ℤ) (-(↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ)) (↑n : ℤ) +
          (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ))
        (⇑α : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K) =
    HSMul.hSMul (β := (a : ↥H) → K) (HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) 1)
        (⇑α : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K)
have e_a : HAdd.hAdd (α := ℤ) 1 (↑n : ℤ) + (↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ) +
      HSub.hSub (α := ℤ) (-(↑(chainTopCoeff (-(⇑α : (a : ↥H) → K)) W) : ℤ)) (↑n : ℤ) +
    (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) =
  HAdd.hAdd (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ) 1
Tactic: congr 2
-- 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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
⊢ False
have H₂ : HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑α : (a : ↥H) → K) +
    (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K) =
  HSMul.hSMul (β := (a : ↥H) → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
Tactic: have H₂ : ((1 + n + chainTopCoeff (-α) W) • α + chainTop (-α) W : H → K) =
      (chainTopCoeff α β + 1) • α + β := by
    simp only [Weight.coe_neg, ← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_add, Nat.cast_one, coe_chainTop,
      smul_neg, ← neg_smul, hW, ← add_assoc, ← add_smul, ← sub_eq_add_neg]
    congr 2
    ring
-- 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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
H₂ :
  HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K) =
    HSMul.hSMul (β := (a : ↥H) → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
⊢ False
have this : rootSpace H
    (-HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑(-α) : (a : ↥H) → K) +
      (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K)) ≠
  ⊥
Tactic: have := rootSpace_neg_nsmul_add_chainTop_of_le (-α) W 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
hα : α.IsNonZero
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
H₁ : 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
H₂ :
  HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K) =
    HSMul.hSMul (β := (a : ↥H) → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) + (⇑β : (a : ↥H) → K)
this :
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) (1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) (⇑(-α) : (a : ↥H) → K) +
        (⇑(chainTop (⇑(-α) : (a : ↥H) → K) W) : (a : ↥H) → K)) ≠
    ⊥
⊢ False
have this₁ : rootSpace H
    (HSMul.hSMul (β := (a : ↥H) → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K)) ≠
  ⊥
Tactic: rw [Weight.coe_neg, ← smul_neg, neg_neg, ← Weight.coe_neg, H₂] at this
Cleared hypotheses: 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
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
have pos : ∀ (hα : α.IsZero), chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
Tactic: by_cases hα : α.IsZero
-- 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
pos : ∀ (hα : α.IsZero), chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
have neg : ∀ (hα : ¬α.IsZero), chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
Tactic: by_cases hα : α.IsZero
-- 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α : ¬α.IsZero
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
have neg : ¬(chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: rw [← not_lt, ← Nat.succ_le_iff]
-- 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α : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ False
have neg : Eq (α := LieSubmodule K (↥H) L)
  (genWeightSpace L
    (HSMul.hSMul (β := ↥H → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β - (chainLength α β).succ) (⇑α : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K)))
  ⊥
Tactic: apply genWeightSpace_nsmul_add_ne_bot_of_le α β
    (Nat.sub_le (chainTopCoeff α β) (chainLength α β).succ)
-- 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α : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β - (chainLength α β).succ) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)))
    ⊥
have neg : Eq (α := LieSubmodule K (↥H) L)
  (genWeightSpace L
    (-HSMul.hSMul (β := ↥H → K) (chainLength α β).succ (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
  ⊥
Tactic: rw [← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_sub e, sub_smul, sub_eq_neg_add,
    add_assoc, ← coe_chainTop, Nat.cast_smul_eq_nsmul]
-- 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
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have pos : ∀ (hα : α.IsZero), chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
Tactic: by_cases hα : α.IsZero
-- 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
pos : ∀ (hα : α.IsZero), chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have neg : ∀ (hα : ¬α.IsZero), chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
Tactic: by_cases hα : α.IsZero
-- 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α : α.IsZero
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have pos : chainBotCoeff 0 β + chainTopCoeff 0 β = chainLength α β
Tactic: rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]
-- 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α : α.IsZero
pos : chainBotCoeff 0 β + chainTopCoeff 0 β = chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have pos₁ : chainBotCoeff 0 β + 0 = chainLength α β
Tactic: rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]
-- 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α : α.IsZero
pos : chainBotCoeff 0 β + chainTopCoeff 0 β = chainLength α β
pos₁ : chainBotCoeff 0 β + 0 = chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have pos₂ : HAdd.hAdd (α := ℕ) 0 0 = chainLength α β
Tactic: rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]
-- 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α : α.IsZero
pos : chainBotCoeff 0 β + chainTopCoeff 0 β = chainLength α β
pos₁ : chainBotCoeff 0 β + 0 = chainLength α β
pos₂ : HAdd.hAdd (α := ℕ) 0 0 = chainLength α β
pos₃ : 0 = chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have pos₄ : Eq (α := ℕ) 0 0
Tactic: rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]
-- 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α : ¬α.IsZero
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have neg : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
Tactic: apply le_antisymm
-- 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α : ¬α.IsZero
neg : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
have neg₁ : chainLength α β ≤ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
Tactic: apply le_antisymm
-- 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α : ¬α.IsZero
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
have neg : ¬(chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
Tactic: rw [← Nat.le_sub_iff_add_le (chainTopCoeff_le_chainLength α β),
      ← not_lt, ← Nat.succ_le_iff, chainBotCoeff, ← Weight.coe_neg]
-- 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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
⊢ False
have neg : Eq (α := LieSubmodule K (↥H) L)
  (genWeightSpace L
    (HSMul.hSMul (β := ↥H → K) (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ (⇑(-α) : (a : ↥H) → K) +
      (⇑β : (a : ↥H) → K)))
  ⊥
Tactic: apply genWeightSpace_nsmul_add_ne_bot_of_le _ _ e
-- 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α : ¬α.IsZero
e : (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ ≤ chainTopCoeff (⇑(-α) : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainLength α β - chainTopCoeff (⇑α : (a : ↥H) → K) β).succ (⇑(-α) : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)))
    ⊥
have neg : Eq (α := LieSubmodule K (↥H) L)
  (genWeightSpace L
    (-HSMul.hSMul (β := ↥H → K) (chainLength α β + 1) (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
  ⊥
Tactic: rw [← Nat.cast_smul_eq_nsmul ℤ, Nat.cast_succ, Nat.cast_sub (chainTopCoeff_le_chainLength α β),
      LieModule.Weight.coe_neg, smul_neg, ← neg_smul, neg_add_rev, neg_sub, sub_eq_neg_add,
      ← add_assoc, ← neg_add_rev, add_smul, add_assoc, ← coe_chainTop, neg_smul,
      ← @Nat.cast_one ℤ, ← Nat.cast_add, Nat.cast_smul_eq_nsmul]
-- 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α : ¬α.IsZero
⊢ chainLength α β ≤ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β
have neg : ¬chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
Tactic: rw [← 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
hα : ¬α.IsZero
e : chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β < chainLength α β
⊢ False
have neg : rootSpace H
    (-HSMul.hSMul (β := (a : ↥H) → K) (chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β).succ
          (⇑α : (a : ↥H) → K) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
  ⊥
Tactic: apply rootSpace_neg_nsmul_add_chainTop_of_le α β e