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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₆ : Eq.{u_1 + 1} (α := K) 0 (↑(0 - HMul.hMul (α := ℤ) 2 0) : K)
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
pos₆ : Eq.{u_1 + 1} (α := K) 0 (↑(0 - HMul.hMul (α := ℤ) 2 0) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₇ : Eq.{u_1 + 1} (α := K) 0 (↑(HSub.hSub (α := ℤ) 0 0) : K)
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
pos₆ : Eq.{u_1 + 1} (α := K) 0 (↑(0 - HMul.hMul (α := ℤ) 2 0) : K)
pos₇ : Eq.{u_1 + 1} (α := K) 0 (↑(HSub.hSub (α := ℤ) 0 0) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₈ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
pos₆ : Eq.{u_1 + 1} (α := K) 0 (↑(0 - HMul.hMul (α := ℤ) 2 0) : K)
pos₇ : Eq.{u_1 + 1} (α := K) 0 (↑(HSub.hSub (α := ℤ) 0 0) : K)
pos₈ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos₉ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength, dif_pos hα, hα.eq, chainTopCoeff_zero, map_zero,
      CharP.cast_eq_zero, mul_zero, sub_self, Int.cast_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
hα : ¬α.IsZero
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have neg : ∀ (x : L)
  (hx :
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x)
  (x_ne0 : x ≠ 0),
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
Tactic: obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero
-- 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α : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have this : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆
Tactic: have := chainLength_smul _ _ hx
-- 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α : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have this₁ : (↑(chainLength α β) : K) =
  HAdd.hAdd (β := K) (HMul.hMul (α := K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : K) 2)
    ((β : (a : ↥H) → K) (coroot α) : K)
Tactic: rw [lie_eq_smul_of_mem_rootSpace hx, ← sub_eq_zero, ← sub_smul,
    smul_eq_zero_iff_left x_ne0, sub_eq_zero, coe_chainTop', nsmul_eq_mul, Pi.natCast_def,
    Pi.add_apply, Pi.mul_apply, root_apply_coroot 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
n : ℕ
hn : n ≤ chainLength α β
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have pos : ∀ (hα : α.IsZero),
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
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
n : ℕ
hn : n ≤ chainLength α β
pos :
  ∀ (hα : α.IsZero),
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have neg : ∀ (hα : ¬α.IsZero),
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have neg : ∀ (x : L)
  (hx :
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x)
  (x_ne0 : x ≠ 0),
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
Tactic: obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have neg : ∀ (h e f : L) (isSl2 : IsSl2Triple h e f) (he : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
  (hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
  rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (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))
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (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) β) : (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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (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
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α β) : K)
Tactic: have prim : isSl2.HasPrimitiveVectorWith x (chainLength α β : 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (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 α β) : K)
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥
have neg : ∃ (x : L) (_ :
  x ∈
    rootSpace H
      (HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))),
  ¬x = 0
Tactic: simp only [← smul_neg, ne_eq, LieSubmodule.eq_bot_iff, not_forall]
-- 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
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥
have by_contra : ∀
  (e :
    ¬rootSpace H
          (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) +
            (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
        ⊥),
  False
Tactic: by_contra e
-- 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 }
⊢ False
have hW : (⇑W : (a : ↥H) → K) =
  -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
Tactic: have hW : (W : H → K) = -(n • α) + chainTop α β := rfl
-- 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)
⊢ 1 + n + chainTopCoeff (⇑(-α) : (a : ↥H) → K) W ≤ chainLength (-α) W
have this : Eq.{u_1 + 1} (α := K) ((W : (a : ↥H) → K) (coroot (-α)) : K)
  ((↑((↑(chainLength (-α) W) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) : ℤ)) : K) : K)
Tactic: have := apply_coroot_eq_cast' (-α) W