awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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) β) : ℤ))
⊢ 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

Premises used: LieAlgebra.IsKilling.chainTopCoeff_zero_right, LieAlgebra.IsKilling.chainBotCoeff_zero_right, Nat.cast_one
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 (-1) 1)
    (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
⊢ let k' := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ);
  k = (↑k' : K)

Tactic:
set k' : ℤ := n - chainTopCoeff α β

Premises used: LieModule.chainTopCoeff, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 (-1) 1)
    (HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ))
H₁ :
  let k' := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ);
  k = (↑k' : K)
⊢ let k' := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ);
  Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'

Tactic:
set k' : ℤ := n - chainTopCoeff α β

Premises used: LieModule.chainTopCoeff, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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'
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
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
subst H
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
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)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'

Tactic:
this

Premises used: Set.Mem, setOf
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
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)
⊢ Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'

Tactic:
exact this
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
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)
⊢ Membership.mem (γ := Finset ℤ) {-1, 0, 1} k'

Tactic:
have : k' ∈ ({-1, 0, 1} : Finset ℤ) := by
      change k' ∈ Finset.Icc (-1 : ℤ) (1 : ℤ)
      exact this
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : α.IsNonZero
h_1 : Nontrivial L
n : ℕ
hn : chainLength α β = n + n
k' : ℤ := HSub.hSub (α := ℤ) (↑n : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)
this_1 : Membership.mem (γ := Finset ℤ) (Finset.Icc (-1) 1) k'
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (↑k' : K) (⇑α : (a : ↥H) → K)
this : Membership.mem (γ := Finset ℤ) {-1, 0, 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:
simpa only [Int.reduceNeg, Finset.mem_insert, Finset.mem_singleton, ← @Int.cast_inj K,
      Int.cast_zero, Int.cast_neg, Int.cast_one] using this

Premises used: Int.cast_neg, Finset.mem_singleton, Int.cast_inj, Int.cast_zero, Int.reduceNeg, Finset.mem_insert, Int.cast_one
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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
⊢ 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

Premises used: HDiv.hDiv, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 * 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

Premises used: smul_eq_mul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 = HAdd.hAdd (α := K) (↑n : K) 2⁻¹ - (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : K)

Tactic:
simpa [sub_div, add_div] using H

Premises used: sub_div, add_div
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 = 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
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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
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) β) : ℤ)
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
have := (rootSpace_zsmul_add_ne_bot_iff α β hα (chainTopCoeff α β - n)).mpr ?_
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 :
  (↑n : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → 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) β) : ℤ)

Tactic:
simp only [tsub_le_iff_right, le_add_iff_nonneg_right, Nat.cast_nonneg, neg_sub, true_and]

Premises used: le_add_iff_nonneg_right, neg_sub, Nat.cast_nonneg, tsub_le_iff_right, true_and
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 : LE.le (α := ℤ) (↑n : ℤ) (↑(2 * n + 1) : ℤ)
⊢ (↑n : ℤ) ≤
    HAdd.hAdd (α := ℤ) (↑(chainBotCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ) (↑(chainTopCoeff (⇑α : (a : ↥H_1) → K) β) : ℤ)

Tactic:
rw [← Nat.cast_add, chainBotCoeff_add_chainTopCoeff, hn]

Premises used: Nat.cast_add, LieAlgebra.IsKilling.chainBotCoeff_add_chainTopCoeff
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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)
⊢ LE.le (α := ℤ) (↑n : ℤ) (↑(2 * n + 1) : ℤ)

Tactic:
lia
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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)) ≠
    ⊥
⊢ 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

Premises used: add_smul, Int.cast_smul_eq_zsmul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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)) ≠
    ⊥
⊢ ¬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

Premises used: Int.cast_natCast, add_sub_cancel_left, Int.cast_sub, sub_add_sub_cancel', ne_eq
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H_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 (α := K) (β := (a : ↥H_1) → K) 2⁻¹ (⇑α : (a : ↥H_1) → K)) = ⊥
⊢ k = -1 ∨ k = 0 ∨ k = 1

Tactic:
cases this (rootSpace_one_div_two_smul α hα)

Premises used: LieAlgebra.IsKilling.rootSpace_one_div_two_smul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
pos : ∀ (hα : α.IsZero), β = -α ∨ β = α
neg : ∀ (hα : ¬α.IsZero), β = -α ∨ β = α
⊢ β = -α ∨ β = α

Tactic:
by_cases hα : α.IsZero

Premises used: LieModule.Weight.IsZero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
hα : α.IsZero
⊢ Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0

Tactic:
rw [hα, smul_zero] at h

Premises used: smul_zero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (β := (a : ↥H) → K) k (⇑α : (a : ↥H) → K)
hα : α.IsZero
h₁ : Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0
⊢ α.IsZero

Tactic:
rw [hα, smul_zero] at h

Premises used: smul_zero
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
k : K
h : Eq (α := (a : ↥H) → K) (⇑β : (a : ↥H) → K) 0
hα : α.IsZero
⊢ β = -α ∨ β = α

Tactic:
cases hβ h
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
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)), β = -α ∨ β = α
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)

Premises used: LieAlgebra.IsKilling.eq_neg_one_or_eq_zero_or_eq_one_of_eq_smul, rfl
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)
h₁ : ∀ (x : ↥H), Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((-α : (a : ↥H) → K) x : K)
⊢ β = -α

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
hα : ¬α.IsZero
h : (⇑β : (a : ↥H) → K) = HSMul.hSMul (α := K) (β := (a : ↥H) → K) (-1) (⇑α : (a : ↥H) → K)
x : ↥H
h₁ : Eq.{u_1 + 1} (α := K) ((-(⇑α : (a : ↥H) → K)) x : K) ((-α : (a : ↥H) → K) x : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) x : K) ((-α : (a : ↥H) → K) x : K)

Tactic:
rw [h, neg_one_smul]

Premises used: neg_one_smul
-- Module: Mathlib.Algebra.Lie.Weights.RootSystem
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hβ : β.IsNonZero
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)

Tactic:
rfl