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
inst_8 : Nontrivial L
hα : α.IsNonZero
h₁ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 ≠ 0
⊢ 1 ≤ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0

Tactic:
rw [Nat.one_le_iff_ne_zero]

Premises used: Nat.one_le_iff_ne_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
inst_8 : Nontrivial L
hα : α.IsNonZero
e : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 = 0
⊢ False

Tactic:
exact α.2 (by simpa [e, Weight.coe_zero] using
      genWeightSpace_chainTopCoeff_add_one_nsmul_add α (0 : Weight K H L) hα)

Premises used: 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
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
h₂ :
  ∀ (h e f : L) (isSl2 : IsSl2Triple h e f) (he : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))),
    ¬1 < 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

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
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
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
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 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) 0) : (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
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 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 α 0) : K)

Tactic:
have prim : isSl2.HasPrimitiveVectorWith x (chainLength α (0 : Weight K H L) : 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
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 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 α 0) : K)
⊢ Membership.mem (α := L) (γ := LieSubmodule K (↥H) L)
    (genWeightSpace L
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
          (-(⇑α : (a : ↥H) → K)) +
        (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)))
    ((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) :
          (a : L) → L)
        x :
      L)

Tactic:
toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1)

Premises used: LieAlgebra.toEnd_pow_apply_mem, HAdd.hAdd, OfNat.ofNat, 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 : 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 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 α 0) : K)
h :
  -(⇑α : (a : ↥H) → K) =
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1)
        (-(⇑α : (a : ↥H) → K)) +
      (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)
⊢ Membership.mem (α := L) (rootSpace H (-(⇑α : (a : ↥H) → K)))
    ((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) :
          (a : L) → L)
        x :
      L)

Tactic:
convert! toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2

Premises used: LieAlgebra.toEnd_pow_apply_mem, HAdd.hAdd, OfNat.ofNat, 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 : 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 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 α 0) : K)
⊢ Membership.mem (α := L) (rootSpace H (-(⇑α : (a : ↥H) → K)))
    ((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) :
          (a : L) → L)
        x :
      L)

Tactic:
have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) := by
      convert! toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2
      rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_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
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 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 α 0) : K)
this :
  Membership.mem (α := L) (rootSpace H (-(⇑α : (a : ↥H) → K)))
    ((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) :
          (a : L) → L)
        x :
      L)
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑(-α) : (a : ↥H) → K)) f hf ≠ 0

Tactic:
simpa using isSl2.f_ne_zero

Premises used: IsSl2Triple.f_ne_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
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 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 α 0) : K)
this :
  Membership.mem (α := L) (rootSpace H (-(⇑α : (a : ↥H) → K)))
    ((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) :
          (a : L) → L)
        x :
      L)
⊢ ∃ (k : K),
    k • f =
      (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) :
          (a : L) → L)
        x

Tactic:
simpa using (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simpa using isSl2.f_ne_zero)).mp
      (finrank_rootSpace_eq_one _ hα.neg) ⟨_, this⟩

Premises used: LieModule.Weight.IsNonZero.neg, Subtype.mk, Iff.mp, LieAlgebra.IsKilling.finrank_rootSpace_eq_one, 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
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 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 α 0) : K)
h₂ :
  ∀ (k : K)
    (hk :
      k • f =
        (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) :
            (a : L) → L)
          x),
    ¬1 < 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

Tactic:
obtain ⟨k, hk⟩ : ∃ k : K, k • f =
      (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x := by
    have : (toEnd K L L f ^ (chainTopCoeff α (0 : Weight K H L) + 1)) x ∈ rootSpace H (-α) := by
      convert! toEnd_pow_apply_mem hf hx (chainTopCoeff α (0 : Weight K H L) + 1) using 2
      rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
    simpa using (finrank_eq_one_iff_of_nonzero' ⟨f, hf⟩ (by simpa using isSl2.f_ne_zero)).mp
      (finrank_rootSpace_eq_one _ hα.neg) ⟨_, this⟩

Premises used: HPow.hPow, HAdd.hAdd, LieModule.toEnd, OfNat.ofNat, 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 : 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 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 α 0) : K)
k : K
hk :
  k • f =
    (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) :
        (a : L) → L)
      x
⊢ ⁅f, k • f⁆ =
    ⁅f,
      (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) :
          (a : L) → L)
        x⁆

Tactic:
apply_fun (⁅f, ·⁆) at hk

Premises used: Bracket.bracket
-- 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
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 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 α 0) : K)
k : K
hk :
  ⁅f, k • f⁆ =
    ⁅f,
      (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) :
          (a : L) → L)
        x⁆
⊢ 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)

Tactic:
simp only [lie_smul, lie_self, smul_zero, prim.lie_f_pow_toEnd_f] at hk

Premises used: lie_smul, smul_zero, lie_self, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f
-- 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
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
⊢ False

Tactic:
prim.pow_toEnd_f_ne_zero_of_eq_nat rfl ?_ hk.symm

Premises used: Eq.symm, 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
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
h₂ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
⊢ False

Tactic:
refine prim.pow_toEnd_f_ne_zero_of_eq_nat rfl ?_ hk.symm

Premises used: Eq.symm, 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
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
⊢ Eq.{u_1 + 1} (α := K)
    ((↑((↑(chainLength α 0) : ℤ) -
            HMul.hMul (α := ℤ) 2
              (↑(chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0) : ℤ)) :
        K) :
      K)
    ((0 : (a : ↥H) → K) (coroot α) : K)

Tactic:
have := (apply_coroot_eq_cast' α 0).symm
-- 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
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 :
  Eq.{u_1 + 1} (α := K)
    ((↑((↑(chainLength α 0) : ℤ) -
            HMul.hMul (α := ℤ) 2
              (↑(chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0) : ℤ)) :
        K) :
      K)
    ((0 : (a : ↥H) → K) (coroot α) : K)
⊢ chainLength α 0 = 2 * chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0

Tactic:
simp only [← @Nat.cast_two ℤ, ← Nat.cast_mul, Weight.zero_apply, Int.cast_eq_zero, sub_eq_zero,
    Nat.cast_inj] at this

Premises used: sub_eq_zero, LieModule.Weight.zero_apply, Nat.cast_inj, Nat.cast_mul, Int.cast_eq_zero, Nat.cast_two
-- 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
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
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
h₅ h₆ h₇ h₈ : 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 + 1 + 1 ≤ chainLength α 0

Tactic:
rwa [this, Nat.succ_le_iff, two_mul, add_lt_add_iff_left]

Premises used: two_mul, Nat.succ_le_iff, add_lt_add_iff_left