awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ 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

Premises used: Int.cast_natCast, zsmul_eq_mul, Pi.mul_apply, LieAlgebra.IsKilling.apply_coroot_eq_cast', Int.cast_sub, LieModule.coe_chainTop, add_sub, sub_eq_neg_add, eq_sub_iff_add_eq, map_neg, Nat.cast_inj, Int.cast_ofNat, Pi.add_apply, Nat.cast_add, Int.cast_mul, sub_eq_iff_eq_add, add_sub_cancel, LieAlgebra.IsKilling.root_apply_coroot, LieAlgebra.IsKilling.coroot_neg, mul_comm, nsmul_eq_mul, OfNat.ofNat, Pi.neg_apply, Pi.natCast_def, mul_two
-- 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
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 :
  chainTopCoeff (⇑(-α) : (a : ↥H) → K) W + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W + (n + n) =
    chainLength (-α) W + chainLength α β
⊢ 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W

Tactic:
lia
-- 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
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)
⊢ 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
-- 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
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
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)
⊢ 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:
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]

Premises used: neg_smul, add_assoc, LieModule.coe_chainTop, sub_eq_add_neg, smul_neg, Int, Nat.cast_add, add_smul, Nat.cast_smul_eq_nsmul, Nat.cast_one, LieModule.Weight.coe_neg
-- 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
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
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
⊢ 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:
congr 2
-- 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
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
⊢ 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:
ring
-- 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
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)

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
-- 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
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)
⊢ 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₁
-- 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
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)) ≠
    ⊥
⊢ 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

Premises used: neg_neg, smul_neg, LieModule.Weight.coe_neg
-- 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
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) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
⊢ False

Tactic:
this (genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα)

Premises used: LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, DFunLike.coe
-- 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
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) (chainTopCoeff (⇑α : (a : ↥H) → K) β + 1) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)) ≠
    ⊥
⊢ False

Tactic:
exact this (genWeightSpace_chainTopCoeff_add_one_nsmul_add α β hα)

Premises used: LieModule.genWeightSpace_chainTopCoeff_add_one_nsmul_add, DFunLike.coe
-- 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
pos : ∀ (hα : α.IsZero), chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
neg : ∀ (hα : ¬α.IsZero), chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- 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
hα : α.IsZero
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β

Tactic:
simp only [hα.eq, chainTopCoeff_zero, zero_le]

Premises used: zero_le, LieModule.Weight.IsZero.eq, LieModule.chainTopCoeff_zero
-- 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
hα : ¬α.IsZero
neg : ¬(chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ chainTopCoeff (⇑α : (a : ↥H) → K) β ≤ chainLength α β

Tactic:
rw [← not_lt, ← Nat.succ_le_iff]

Premises used: not_lt, Nat.succ_le_iff
-- 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
hα : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
neg :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff (⇑α : (a : ↥H) → K) β - (chainLength α β).succ) (⇑α : (a : ↥H) → K) +
        (⇑β : (a : ↥H) → K)))
    ⊥
⊢ False

Tactic:
apply genWeightSpace_nsmul_add_ne_bot_of_le α β
    (Nat.sub_le (chainTopCoeff α β) (chainLength α β).succ)

Premises used: LieModule.genWeightSpace_nsmul_add_ne_bot_of_le, Nat.sub_le, LieAlgebra.IsKilling.chainLength, LieModule.chainTopCoeff, Nat.succ, DFunLike.coe
-- 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
hα : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
neg :
  Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β).succ (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (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)))
    ⊥

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]

Premises used: Nat.cast_sub, add_assoc, LieModule.coe_chainTop, sub_eq_neg_add, sub_smul, Int, Nat.cast_smul_eq_nsmul
-- 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
hα : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β).succ (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⊥

Tactic:
rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)

Premises used: LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, Nat.lt_succ_self
-- 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
hα : ¬α.IsZero
e : (chainLength α β).succ ≤ chainTopCoeff (⇑α : (a : ↥H) → K) β
⊢ Eq (α := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (-HSMul.hSMul (β := ↥H → K) (chainLength α β).succ (⇑α : (a : ↥H) → K) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⊥

Tactic:
exact rootSpace_neg_nsmul_add_chainTop_of_lt α β hα (Nat.lt_succ_self _)

Premises used: LieAlgebra.IsKilling.rootSpace_neg_nsmul_add_chainTop_of_lt, Nat.lt_succ_self
-- 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
pos : ∀ (hα : α.IsZero), chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
neg : ∀ (hα : ¬α.IsZero), chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- 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
hα : α.IsZero
pos : chainBotCoeff 0 β + chainTopCoeff 0 β = chainLength α β
pos₁ : chainBotCoeff 0 β + 0 = chainLength α β
pos₂ : HAdd.hAdd (α := ℕ) 0 0 = chainLength α β
pos₃ : 0 = chainLength α β
pos₄ pos₅ : Eq (α := ℕ) 0 0
⊢ chainBotCoeff (⇑α : (a : ↥H) → K) β + chainTopCoeff (⇑α : (a : ↥H) → K) β = chainLength α β

Tactic:
rw [hα.eq, chainTopCoeff_zero, chainBotCoeff_zero, zero_add, chainLength_of_isZero α β hα]

Premises used: LieModule.Weight.IsZero.eq, zero_add, LieModule.chainBotCoeff_zero, LieModule.chainTopCoeff_zero, LieAlgebra.IsKilling.chainLength_of_isZero