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
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e_1 f : L
he : e_1 ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e_1 f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
k : K
hk :
  Eq (α := L) (0 : L)
    ((HPow.hPow (α := End K L) ((toEnd K L L : (a : L) → End K L) f : End K L)
            (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1) :
          (a : L) → L)
        x :
      L)
e : 1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
this : chainLength α 0 = 2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
have h₂ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤
  2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: rwa [this, Nat.succ_le_iff, two_mul, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e_1 f : L
he : e_1 ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e_1 f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
k : K
hk :
  Eq (α := L) (0 : L)
    ((HPow.hPow (α := End K L) ((toEnd K L L : (a : L) → End K L) f : End K L)
            (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1) :
          (a : L) → L)
        x :
      L)
e : 1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
this : chainLength α 0 = 2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
h₂ :
  chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤
    2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
have h₃ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 <
  2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: rwa [this, Nat.succ_le_iff, two_mul, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e_1 f : L
he : e_1 ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e_1 f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
k : K
hk :
  Eq (α := L) (0 : L)
    ((HPow.hPow (α := End K L) ((toEnd K L L : (a : L) → End K L) f : End K L)
            (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1) :
          (a : L) → L)
        x :
      L)
e : 1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
this : chainLength α 0 = 2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
h₂ :
  chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤
    2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
h₃ :
  chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 <
    2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
have h₄ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 <
  chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 +
    chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
Tactic: rwa [this, Nat.succ_le_iff, two_mul, add_lt_add_iff_left]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
⊢ chainLength α 0 = 2
have rw : chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 +
    chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 =
  2
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α 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
inst_8 : Nontrivial L
hα : α.IsNonZero
rw :
  chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 +
      chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 =
    2
⊢ chainLength α 0 = 2
have rw₁ : chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 = 2
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α 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
inst_8 : Nontrivial L
hα : α.IsNonZero
rw :
  chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 +
      chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 =
    2
rw₁ : chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 = 2
⊢ chainLength α 0 = 2
have rw₂ : HAdd.hAdd (α := ℕ) 1 1 = 2
Tactic: rw [← chainBotCoeff_add_chainTopCoeff, chainTopCoeff_zero_right α hα,
    chainBotCoeff_zero_right α 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α : α.IsNonZero
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
have inl : Subsingleton L → rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
Tactic: cases subsingleton_or_nontrivial L
-- 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
inl : Subsingleton L → rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
⊢ rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
have inr : Nontrivial L → rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑α : (a : ↥H) → K)) = ⊥
Tactic: cases subsingleton_or_nontrivial L
-- 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
⊢ rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
have by_contra : ∀ (h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥), False
Tactic: by_contra 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α : α.IsNonZero
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
⊢ HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
have change : HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = (⇑α : (a : ↥H) → K)
Tactic: change 2 • (2⁻¹ : K) • (α : H → K) = α
-- 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
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
⊢ HSMul.hSMul (α := ℕ) 2 (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = (⇑α : (a : ↥H) → K)
have rw : HSMul.hSMul (β := (a : ↥H) → K) (HMul.hMul (α := K) (↑2 : K) 2⁻¹) (⇑α : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
Tactic: rw [← Nat.cast_smul_eq_nsmul K, smul_smul]
-- 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
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
⊢ False
have hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
Tactic: have hW : 2 • (W : H → K) = α := by
    change 2 • (2⁻¹ : K) • (α : H → K) = α
    rw [← Nat.cast_smul_eq_nsmul K, smul_smul]; simp
-- 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
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
⊢ False
have apply : Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
Tactic: apply α.genWeightSpace_ne_bot
-- 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
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
e : Eq (α := (a : ↥H) → K) (⇑W : (a : ↥H) → K) 0
⊢ α.IsZero
have e₁ : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 0
Tactic: apply_fun (2 • ·) at e
Cleared hypotheses: 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
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
⊢ Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
have this : rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K)) = ⊥
Tactic: have := rootSpace_two_smul W (fun (e : (W : H → K) = 0) ↦ hα <| by
    apply_fun (2 • ·) at e; simpa [hW] using 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α : α.IsNonZero
h : ¬rootSpace H (HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K)) = ⊥
W : Weight K (↥H) L :=
  { toFun := HSMul.hSMul (α := K) (β := (a : ↥H) → K) 2⁻¹ (⇑α : (a : ↥H) → K), genWeightSpace_ne_bot' := h }
hW : HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K) = (⇑α : (a : ↥H) → K)
this : rootSpace H (HSMul.hSMul (α := ℕ) (β := (a : ↥H) → K) 2 (⇑W : (a : ↥H) → K)) = ⊥
⊢ Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
have rwa : ∀ (this : rootSpace H (⇑α : (a : ↥H) → K) = ⊥), Eq (α := LieSubmodule K (↥H) L) (genWeightSpace L (⇑α : (a : ↥H) → K)) ⊥
Tactic: rwa [hW] 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
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inl : Subsingleton L → k = -1 ∨ k = 0 ∨ k = 1
Tactic: cases subsingleton_or_nontrivial L
-- 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
inl : Subsingleton L → k = -1 ∨ k = 0 ∨ k = 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr : Nontrivial L → k = -1 ∨ k = 0 ∨ k = 1
Tactic: cases subsingleton_or_nontrivial L
-- 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
h_1 : Nontrivial L
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
  ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
Tactic: have H := apply_coroot_eq_cast' α β
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H_1) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K) (coroot α) =
  (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
Tactic: rw [h] at H
Cleared hypotheses: 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K) (coroot α) =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : HSMul.hSMul (β := K) k 2 =
  (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
Tactic: simp only [Pi.smul_apply, root_apply_coroot hα] at H
Cleared hypotheses: 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr : ∀ (n : ℕ) (hn : chainLength α β = n + n), k = -1 ∨ k = 0 ∨ k = 1
Tactic: rcases (chainLength α β).even_or_odd with (⟨n, hn⟩ | ⟨n, hn⟩)
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
inr : ∀ (n : ℕ) (hn : chainLength α β = n + n), k = -1 ∨ k = 0 ∨ k = 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr₁ : ∀ (n : ℕ) (hn : chainLength α β = 2 * n + 1), k = -1 ∨ k = 0 ∨ k = 1
Tactic: rcases (chainLength α β).even_or_odd with (⟨n, hn⟩ | ⟨n, hn⟩)
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
n : ℕ
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : HSMul.hSMul (β := K) k 2 = (↑((↑(2 * n) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
Tactic: rw [hn, ← two_mul] at H
Cleared hypotheses: H, hn
-- 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
H :
  HSMul.hSMul (β := K) k 2 =
    (↑((↑(2 * n) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
hn : chainLength α β = n + n
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : k = HSub.hSub (α := K) (↑n : K) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
Tactic: simp only [smul_eq_mul, Nat.cast_mul, Nat.cast_ofNat, ← mul_sub, ← mul_comm (2 : K),
      Int.cast_sub, Int.cast_mul, Int.cast_ofNat, Int.cast_natCast,
      mul_eq_mul_left_iff, OfNat.ofNat_ne_zero, or_false] at H
Cleared hypotheses: 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_1 : LieSubalgebra K L
inst_6 : H_1.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H_1) L
α β : Weight K (↥H_1) L
hα : α.IsNonZero
k : K
h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (β := (a : ↥H_1) → K) k (⇑α : (a : ↥H_1) → K)
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
H : k = HSub.hSub (α := K) (↑n : K) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : k = (↑(HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
Tactic: rw [← Int.cast_natCast, ← Int.cast_natCast (chainTopCoeff α β), ← Int.cast_sub] at H
Cleared hypotheses: H