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_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 (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ rootSpace H_1
      (HSMul.hSMul (β := (a : ↥H_1) → K) (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
          (⇑α : (a : ↥H_1) → K) +
        (⇑0 : (a : ↥H_1) → K)) ≠
    ⊥
have rw : rootSpace H_1 (⇑β : (a : ↥H_1) → K) ≠ ⊥
Tactic: rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, Weight.coe_zero, add_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_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 (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have this : Membership.mem (γ := Finset ℤ)
  (Finset.Icc (-(↑(chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
    (↑(chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
  (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
Tactic: have := (rootSpace_zsmul_add_ne_bot_iff_mem α 0 hα (n - chainTopCoeff α β)).mp
      (by rw [← Int.cast_smul_eq_zsmul K, ← H, ← h, Weight.coe_zero, add_zero]; exact β.2)
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (hypothesis)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
this :
  Membership.mem (γ := Finset ℤ)
    (Finset.Icc (-(↑(chainBotCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
      (↑(chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H_1) (M := L) (⇑α : (a : ↥H_1) → K) 0) : ℤ))
    (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
⊢ k = -1 ∨ k = 0 ∨ k = 1
have this₁ : Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1)
  (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
Tactic: rw [chainTopCoeff_zero_right α hα, chainBotCoeff_zero_right α hα, Nat.cast_one] 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_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
k' : ℤ := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)
H : k = (↑k' : K)
this : Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr : ∀ (h : (⇑β : (a : ↥H_1) → K) = HSMul.hSMul (α := K) (β := (a : ↥H_1) → K) (↑k' : K) (⇑α : (a : ↥H_1) → K)),
  Eq.{u_1 + 1} (α := K) (↑k' : K) (-1) ∨ Eq.{u_1 + 1} (α := K) (↑k' : K) 0 ∨ Eq.{u_1 + 1} (α := K) (↑k' : K) 1
Tactic: subst H
Cleared hypotheses: k, h, 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
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
k' : ℤ := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
this : Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (↑k' : K) (⇑α : (a : ↥H) → K)
⊢ Eq.{u_1 + 1} (α := K) (↑k' : K) (-1) ∨ Eq.{u_1 + 1} (α := K) (↑k' : K) 0 ∨ Eq.{u_1 + 1} (α := K) (↑k' : K) 1
have this₁ : Membership.mem (γ := Finset ℤ) {-1, 0, 1} k'
Tactic: have : k' ∈ ({-1, 0, 1} : Finset ℤ) := by
      change k' ∈ Finset.Icc (-1 : ℤ) (1 : ℤ)
      exact 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_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 α β = 2 * n + 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : HSMul.hSMul (β := K) k 2 / 2 =
  HDiv.hDiv (α := K)
    (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K) 2
Tactic: apply_fun (· / 2) 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 α β = 2 * n + 1
H :
  HSMul.hSMul (β := K) k 2 / 2 =
    HDiv.hDiv (α := K)
      (↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K) 2
⊢ k = -1 ∨ k = 0 ∨ k = 1
have H₁ : k * 2 / 2 =
  HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K) 2
Tactic: rw [hn, smul_eq_mul] 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 α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
⊢ k = -1 ∨ k = 0 ∨ k = 1
have hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
Tactic: have hk : k = n + 2⁻¹ - chainTopCoeff α β := by simpa [sub_div, add_div] using 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
n : ℕ
hn : chainLength α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr : ∀
  (this :
    rootSpace H_1
        (HSMul.hSMul (β := (a : ↥H_1) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ))
            (⇑α : (a : ↥H_1) → K) +
          (⇑β : (a : ↥H_1) → K)) ≠
      ⊥),
  k = -1 ∨ k = 0 ∨ k = 1
Tactic: have := (rootSpace_zsmul_add_ne_bot_iff α β hα (chainTopCoeff α β - n)).mpr ?_
-- 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
n : ℕ
hn : chainLength α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
inr :
  ∀
    (this :
      rootSpace H_1
          (HSMul.hSMul (β := (a : ↥H_1) → K)
              (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ)) (⇑α : (a : ↥H_1) → K) +
            (⇑β : (a : ↥H_1) → K)) ≠
        ⊥),
    k = -1 ∨ k = 0 ∨ k = 1
⊢ k = -1 ∨ k = 0 ∨ k = 1
have inr₁ : HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ) ≤
    (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) ∧
  -HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ) ≤
    (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)
Tactic: have := (rootSpace_zsmul_add_ne_bot_iff α β hα (chainTopCoeff α β - n)).mpr ?_
-- 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
n : ℕ
hn : chainLength α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
⊢ HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ) ≤
      (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) ∧
    -HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ) ≤
      (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)
have inr : (↑n : ℤ) ≤
  HAdd.hAdd (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)
Tactic: simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg, neg_sub, true_and]
-- 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
n : ℕ
hn : chainLength α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
⊢ (↑n : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)
have inr : LE.le (α := ℤ) (↑n : ℤ) (↑(2 * n + 1) : ℤ)
Tactic: rw [← Nat.cast_add, chainBotCoeff_add_chainTopCoeff, 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 : ℕ
hn : chainLength α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
this :
  rootSpace H_1
      (HSMul.hSMul (β := (a : ↥H_1) → K) (HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ))
          (⇑α : (a : ↥H_1) → K) +
        (⇑β : (a : ↥H_1) → K)) ≠
    ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1
have this₁ : rootSpace H_1
    (HSMul.hSMul (β := (a : ↥H_1) → K)
      ((↑(HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ)) : K) +
        (HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)))
      (⇑α : (a : ↥H_1) → K)) ≠
  ⊥
Tactic: rw [h, hk, ← Int.cast_smul_eq_zsmul K, ← add_smul] 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_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 α β = 2 * n + 1
H :
  k * 2 / 2 =
    HDiv.hDiv (α := K) (↑((↑(2 * n + 1) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)) : K)
      2
hk : k = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)
this :
  rootSpace H_1
      (HSMul.hSMul (β := (a : ↥H_1) → K)
        ((↑(HSub.hSub (α := ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑n : ℤ)) : K) +
          (HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)))
        (⇑α : (a : ↥H_1) → K)) ≠
    ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1
have this₁ : ¬rootSpace H_1 (HSMul.hSMul (α := K) (β := (a : ↥H_1) → K) 2⁻¹ (⇑α : (a : ↥H_1) → K)) = ⊥
Tactic: simp only [Int.cast_sub, Int.cast_natCast,
      sub_add_sub_cancel', add_sub_cancel_left, ne_eq] 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)
⊢ β = -α ∨ β = α
have pos : ∀ (hα : α.IsZero), β = -α ∨ β = α
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β : β.IsNonZero
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), β = -α ∨ β = α
⊢ β = -α ∨ β = α
have neg : ∀ (hα : ¬α.IsZero), β = -α ∨ β = α
Tactic: by_cases hα : α.IsZero
-- 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α : α.IsZero
⊢ β = -α ∨ β = α
have h₁ : Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0
Tactic: rw [hα, smul_zero] at h
Cleared hypotheses: h, 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
hα : ¬α.IsZero
⊢ β = -α ∨ β = α
have neg : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
Tactic: rcases eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul α β hα k h with (rfl | rfl | rfl)
Cleared hypotheses: k, 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
hα : ¬α.IsZero
neg : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
⊢ β = -α ∨ β = α
have neg₁ : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 0 (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
Tactic: rcases eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul α β hα k h with (rfl | rfl | rfl)
Cleared hypotheses: k, 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
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
hα : ¬α.IsZero
neg : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
neg₁ : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 0 (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
⊢ β = -α ∨ β = α
have neg₂ : ∀ (h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)), β = -α ∨ β = α
Tactic: rcases eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul α β hα k h with (rfl | rfl | rfl)
Cleared hypotheses: k, 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α : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)
⊢ β = -α
have h₁ : ∀ (x : ↥H), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((-α : (a : ↥H) → K) x : K)
Tactic: ext
-- 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α : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)
x : ↥H
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((-α : (a : ↥H) → K) x : K)
have h₁ : Eq.{u_1 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) ((-α : (a : ↥H) → K) x : K)
Tactic: rw [h, neg_one_smul]
-- 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α : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 0 (⇑α : (a : ↥H) → K)
⊢ β.IsZero
have rwa : ∀ (h : Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0), β.IsZero
Tactic: rwa [zero_smul] 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 : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
⊢ β = α
have h₁ : ∀ (x : ↥H), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
Tactic: ext
-- 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α : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
x : ↥H
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
have h₁ : HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K) x = (α : (a : ↥H) → K) x
Tactic: rw [h, one_smul]
-- 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α : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K)
x : ↥H
h₁ : HSMul.hSMul (α := K) (β := (a : ↥H) → K) 1 (⇑α : (a : ↥H) → K) x = (α : (a : ↥H) → K) x
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
have h₂ : Eq.{u_1 + 1} (α := K) ((α : (a : ↥H) → K) x : K) ((α : (a : ↥H) → K) x : K)
Tactic: rw [h, one_smul]