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α : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
pos : ∀ (hx' : x = 0), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
have neg : ∀ (hx' : ¬x = 0), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
Tactic: by_cases hx' : x = 0
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬x = 0
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
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))), ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
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
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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))
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
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
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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⁆
⊢ ⁅(↑(coroot α) : L), x⁆ =
    HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x
have rw : ⁅(↑(coroot α) : L), x⁆ = ⁅coroot α, x⁆
Tactic: rw [← lie_eq_smul_of_mem_rootSpace hx]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
have this : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
  ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
Tactic: have : isSl2.HasPrimitiveVectorWith x (chainTop α β (coroot α)) :=
    have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
    ⟨hx', by rw [← lie_eq_smul_of_mem_rootSpace hx]; rfl,
      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
hα : α.IsNonZero
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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 :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
⊢ ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
have neg : ∀ (μ : ℕ) (hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)),
  ∃ (n : ℕ), n • x = ⁅coroot α, x⁆
Tactic: obtain ⟨μ, hμ⟩ := this.exists_nat
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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 :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
μ : ℕ
hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)
⊢ μ • x = ⁅coroot α, x⁆
have rw : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑μ : K) x = ⁅coroot α, x⁆
Tactic: rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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 :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
μ : ℕ
hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑μ : K) x = ⁅coroot α, x⁆
⊢ μ • x = ⁅coroot α, x⁆
have rw₁ : HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x = ⁅coroot α, x⁆
Tactic: rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hx' : ¬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 :
  IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x
    ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K)
μ : ℕ
hμ : Eq.{u_1 + 1} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) ((↑μ : K) : K)
rw : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑μ : K) x = ⁅coroot α, x⁆
rw₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x =
    ⁅coroot α, x⁆
⊢ μ • x = ⁅coroot α, x⁆
have rw₂ : HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x =
  HSMul.hSMul.{u_1, u_2, u_2} (α := K) ((chainTop (⇑α : (a : ↥H) → K) β : (a : ↥H) → K) (coroot α) : K) x
Tactic: rw [← Nat.cast_smul_eq_nsmul K, ← hμ, lie_eq_smul_of_mem_rootSpace hx]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ chainLength α β • x = ⁅coroot α, x⁆
have pos : ∀ (hα : α.IsZero), chainLength α β • x = ⁅coroot α, x⁆
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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), chainLength α β • x = ⁅coroot α, x⁆
⊢ chainLength α β • x = ⁅coroot α, x⁆
have neg : ∀ (hα : ¬α.IsZero), chainLength α β • x = ⁅coroot α, x⁆
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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : α.IsZero
⊢ chainLength α β • x = ⁅coroot α, x⁆
have pos : chainLength α β • x = Bracket.bracket (L := ↥H) 0 x
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : α.IsZero
pos : chainLength α β • x = Bracket.bracket (L := ↥H) 0 x
⊢ chainLength α β • x = ⁅coroot α, x⁆
have pos₁ : HSMul.hSMul (α := ℕ) 0 x = Bracket.bracket (L := ↥H) 0 x
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : α.IsZero
pos : chainLength α β • x = Bracket.bracket (L := ↥H) 0 x
pos₁ : HSMul.hSMul (α := ℕ) 0 x = Bracket.bracket (L := ↥H) 0 x
⊢ chainLength α β • x = ⁅coroot α, x⁆
have pos₂ : 0 = Bracket.bracket (L := ↥H) 0 x
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : α.IsZero
pos : chainLength α β • x = Bracket.bracket (L := ↥H) 0 x
pos₁ : HSMul.hSMul (α := ℕ) 0 x = Bracket.bracket (L := ↥H) 0 x
pos₂ : 0 = Bracket.bracket (L := ↥H) 0 x
⊢ chainLength α β • x = ⁅coroot α, x⁆
have pos₃ : Eq.{u_2 + 1} (α := L) 0 0
Tactic: rw [coroot_eq_zero_iff.mpr hα, chainLength_of_isZero _ _ hα, zero_smul, zero_lie]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : ¬α.IsZero
x' : L :=
  ⋯.choose (p := fun (x : L) ↦
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x ∧
      x ≠ 0)
⊢ chainLength α β • x = ⁅coroot α, x⁆
have h : x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ∧ x' ≠ 0
Tactic: have h : x' ∈ rootSpace H (chainTop α β) ∧ x' ≠ 0 :=
    (chainTop α β).exists_ne_zero.choose_spec
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
hα : ¬α.IsZero
x' : L :=
  ⋯.choose (p := fun (x : L) ↦
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x ∧
      x ≠ 0)
h : x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ∧ x' ≠ 0
⊢ chainLength α β • x = ⁅coroot α, x⁆
have neg : ∀ (k : K) (hx : k • x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)),
  chainLength α β • k • x' = ⁅coroot α, k • x'⁆
Tactic: obtain ⟨k, rfl⟩ : ∃ k : K, k • x' = x := by
    simpa using (finrank_eq_one_iff_of_nonzero' ⟨x', h.1⟩ (by simpa using h.2)).mp
      (finrank_rootSpace_eq_one _ (chainTop_isNonZero α β hα)) ⟨_, hx⟩
Cleared hypotheses: x, hx
-- 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
x' : L :=
  ⋯.choose (p := fun (x : L) ↦
    Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x ∧
      x ≠ 0)
h : x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K) ∧ x' ≠ 0
k : K
hx : k • x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ chainLength α β • k • x' = ⁅coroot α, k • x'⁆
have neg : k • HSMul.hSMul (α := ℕ) sorry x' = k • ⁅coroot α, x'⁆
Tactic: rw [lie_smul, smul_comm, chainLength, dif_neg hα, (chainLength_aux α β hα h.1).choose_spec]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆
have rw : chainLength α β • x = ⁅coroot α, x⁆
Tactic: rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
rw : chainLength α β • x = ⁅coroot α, x⁆
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆
have rw₁ : ⁅coroot α, x⁆ = ⁅coroot α, x⁆
Tactic: rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]
-- 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
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have pos : ∀ (hα : α.IsZero),
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : 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
pos :
  ∀ (hα : α.IsZero),
    Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
      ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
have neg : ∀ (hα : ¬α.IsZero),
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : 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
hα : α.IsZero
⊢ 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)
  ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : 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)
⊢ 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)
  ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
      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)
⊢ 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 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : 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)
⊢ 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 (↑(chainTopCoeff 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]