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 : 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
⊢ ∃ (k : K), k • x' = x

Tactic:
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⟩

Premises used: Subtype.mk, Iff.mp, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, LieModule.chainTop_isNonZero, finrank_eq_one_iff_of_nonzero'
-- 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
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
neg :
  ∀ (k : K) (hx : k • x' ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)),
    chainLength α β • k • x' = ⁅coroot α, k • x'⁆
⊢ chainLength α β • x = ⁅coroot α, 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⟩

Premises used: 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α : ¬α.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)
neg : k • HSMul.hSMul (α := ℕ) sorry x' = k • ⁅coroot α, x'⁆
⊢ chainLength α β • k • x' = ⁅coroot α, k • x'⁆

Tactic:
rw [lie_smul, smul_comm, chainLength, dif_neg hα, (chainLength_aux α β hα h.1).choose_spec]

Premises used: Exists.choose_spec, lie_smul, _private.0.LieAlgebra.IsKilling.chainLength_aux, dif_neg, And.left, SMulCommClass.smul_comm, LieAlgebra.IsKilling.chainLength
-- 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
x : L
hx : x ∈ rootSpace H (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
rw : chainLength α β • x = ⁅coroot α, x⁆
rw₁ rw₂ : ⁅coroot α, x⁆ = ⁅coroot α, x⁆
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆

Tactic:
rw [Nat.cast_smul_eq_nsmul, chainLength_nsmul _ _ hx]

Premises used: LieAlgebra.IsKilling.chainLength_nsmul, Nat.cast_smul_eq_nsmul
-- 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
pos :
  ∀ (hα : α.IsZero),
    Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
      ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
neg :
  ∀ (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)

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α : α.IsZero
pos :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₁ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑(if hα : α.IsZero then 0 else sorry) : ℤ) -
            HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) :
        K) :
      K)
pos₂ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
pos₃ :
  Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K)
    ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff 0 β) : ℤ)) : K) : K)
pos₄ : Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) 0 : K) ((↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K) : K)
pos₅ : Eq.{u_1 + 1} (α := K) 0 (↑((↑0 : ℤ) - HMul.hMul (α := ℤ) 2 (↑0 : ℤ)) : K)
pos₆ : Eq.{u_1 + 1} (α := K) 0 (↑(0 - HMul.hMul (α := ℤ) 2 0) : K)
pos₇ : Eq.{u_1 + 1} (α := K) 0 (↑(HSub.hSub (α := ℤ) 0 0) : K)
pos₈ : Eq.{u_1 + 1} (α := K) 0 (↑0 : K)
pos₉ pos₁₀ : Eq.{u_1 + 1} (α := K) 0 0
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : 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]

Premises used: CharP.cast_eq_zero, Iff.mpr, sub_self, Int.cast_zero, LieModule.Weight.IsZero.eq, map_zero, dif_pos, MulZeroClass.mul_zero, LieAlgebra.IsKilling.coroot_eq_zero_iff, LieModule.chainTopCoeff_zero, LieAlgebra.IsKilling.chainLength
-- 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α : ¬α.IsZero
neg :
  ∀ (x : L)
    (hx :
      Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x)
    (x_ne0 : x ≠ 0),
    Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
      ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)

Tactic:
obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero

Premises used: LieModule.Weight.exists_ne_zero, LieModule.chainTop, 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 : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
⊢ HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆

Tactic:
have := chainLength_smul _ _ hx
-- 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α : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this : HSMul.hSMul.{u_1, u_2, u_2} (α := K) (↑(chainLength α β) : K) x = ⁅coroot α, x⁆
⊢ (↑(chainLength α β) : K) =
    HAdd.hAdd (β := K) (HMul.hMul (α := K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : K) 2)
      ((β : (a : ↥H) → K) (coroot α) : K)

Tactic:
rw [lie_eq_smul_of_mem_rootSpace hx, ← sub_eq_zero, ← sub_smul,
    smul_eq_zero_iff_left x_ne0, sub_eq_zero, coe_chainTop', nsmul_eq_mul, Pi.natCast_def,
    Pi.add_apply, Pi.mul_apply, root_apply_coroot hα] at this

Premises used: Pi.mul_apply, sub_eq_zero, sub_smul, smul_eq_zero_iff_left, Pi.add_apply, LieAlgebra.IsKilling.lie_eq_smul_of_mem_rootSpace, LieAlgebra.IsKilling.root_apply_coroot, nsmul_eq_mul, Pi.natCast_def, LieModule.coe_chainTop'
-- 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α : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
this :
  (↑(chainLength α β) : K) =
    HAdd.hAdd (β := K) (HMul.hMul (α := K) (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : K) 2)
      ((β : (a : ↥H) → K) (coroot α) : K)
⊢ Eq.{u_1 + 1} (α := K) ((β : (a : ↥H) → K) (coroot α) : K)
    ((↑((↑(chainLength α β) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑α : (a : ↥H) → K) β) : ℤ)) : K) : K)

Tactic:
simp only [Int.cast_sub, Int.cast_natCast, Int.cast_mul, Int.cast_ofNat, eq_sub_iff_add_eq',
    this, mul_comm (2 : K)]

Premises used: eq_sub_iff_add_eq', Int.cast_natCast, Int.cast_sub, Int.cast_ofNat, Int.cast_mul, mul_comm, 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 : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
pos :
  ∀ (hα : α.IsZero),
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
      ⊥
neg :
  ∀ (hα : ¬α.IsZero),
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥

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
n : ℕ
hn : n ≤ chainLength α β
hα : α.IsZero
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥

Tactic:
simpa only [hα.eq, smul_zero, neg_zero, chainTop_zero, zero_add, ne_eq] using β.2

Premises used: LieModule.chainTop_zero, LieModule.Weight.IsZero.eq, smul_zero, zero_add, ne_eq, neg_zero, LieModule.Weight.genWeightSpace_ne_bot'
-- 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
neg :
  ∀ (x : L)
    (hx :
      Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))
        x)
    (x_ne0 : x ≠ 0),
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥

Tactic:
obtain ⟨x, hx, x_ne0⟩ := (chainTop α β).exists_ne_zero

Premises used: LieModule.Weight.exists_ne_zero, LieModule.chainTop, 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 : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
neg :
  ∀ (h e f : L) (isSl2 : IsSl2Triple h e f) (he : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
    rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
      ⊥
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥

Tactic:
obtain ⟨h, e, f, isSl2, he, hf⟩ := exists_isSl2Triple_of_weight_isNonZero hα

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
h e f : L
isSl2 : IsSl2Triple h e f
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ IsSl2Triple (↑(coroot α) : L) e f

Tactic:
obtain rfl := isSl2.h_eq_coroot hα he hf

Premises used: IsSl2Triple.h_eq_coroot, 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
this :
  Membership.mem (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L (HAdd.hAdd (α := ↥H → K) (⇑α : (a : ↥H) → K) (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)))
    ⁅e, x⁆
rwa rwa₁ rwa₂ rwa₃ : ∀ (this : Membership.mem (γ := LieSubmodule K (↥H) L) ⊥ ⁅e, x⁆), ⁅e, x⁆ = 0
⊢ ⁅e, x⁆ = 0

Tactic:
rwa [genWeightSpace_add_chainTop _ _ hα] at this

Premises used: LieModule.genWeightSpace_add_chainTop
-- 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
⊢ IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α β) : K)

Tactic:
have prim : isSl2.HasPrimitiveVectorWith x (chainLength α β : K) :=
    have := lie_mem_genWeightSpace_of_mem_genWeightSpace he hx
    ⟨x_ne0, (chainLength_smul _ _ hx).symm, by rwa [genWeightSpace_add_chainTop _ _ hα] at this⟩
-- 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α β) : K)
neg :
  ∃ (x : L) (_ :
    x ∈
      rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) +
          (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))),
    ¬x = 0
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) ≠
    ⊥

Tactic:
simp only [← smul_neg, ne_eq, LieSubmodule.eq_bot_iff, not_forall]

Premises used: smul_neg, ne_eq, Classical.not_forall, LieSubmodule.eq_bot_iff
-- 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α β) : K)
⊢ ∃ (x : L) (_ :
    x ∈
      rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) +
          (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))),
    ¬x = 0

Tactic:
⟨_, toEnd_pow_apply_mem hf hx n, prim.pow_toEnd_f_ne_zero_of_eq_nat rfl hn⟩

Premises used: LieAlgebra.toEnd_pow_apply_mem, Exists.intro, IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_ne_zero_of_eq_nat, 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
n : ℕ
hn : n ≤ chainLength α β
hα : ¬α.IsZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e f : L
he : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α β) : K)
⊢ ∃ (x : L) (_ :
    x ∈
      rootSpace H
        (HSMul.hSMul (β := (a : ↥H) → K) n (-(⇑α : (a : ↥H) → K)) +
          (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K))),
    ¬x = 0

Tactic:
exact ⟨_, toEnd_pow_apply_mem hf hx n, prim.pow_toEnd_f_ne_zero_of_eq_nat rfl hn⟩
-- 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
n : ℕ
hn : chainLength α β < n
by_contra :
  ∀
    (e :
      ¬rootSpace H
            (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) +
              (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
          ⊥),
    False
⊢ rootSpace H
      (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
    ⊥

Tactic:
by_contra e
-- 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
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
⊢ (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)

Tactic:
have hW : (W : H → K) = -(n • α) + chainTop α β := rfl
-- 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
n : ℕ
hn : chainLength α β < n
e :
  ¬rootSpace H
        (-HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)) =
      ⊥
W : Weight K (↥H) L :=
  {
    toFun :=
      -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K),
    genWeightSpace_ne_bot' := e }
hW :
  (⇑W : (a : ↥H) → K) =
    -HSMul.hSMul (β := (a : ↥H) → K) n (⇑α : (a : ↥H) → K) + (⇑(chainTop (⇑α : (a : ↥H) → K) β) : (a : ↥H) → K)
⊢ Eq.{u_1 + 1} (α := K) ((W : (a : ↥H) → K) (coroot (-α)) : K)
    ((↑((↑(chainLength (-α) W) : ℤ) - HMul.hMul (α := ℤ) 2 (↑(chainTopCoeff (⇑(-α) : (a : ↥H) → K) W) : ℤ)) : K) : K)

Tactic:
have := apply_coroot_eq_cast' (-α) W