awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → K))
⊢ -(⇑α : (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)
have 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)) +
    (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K) +
      0)
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        0)
⊢ -(⇑α : (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)
have 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)) +
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
      (⇑α : (a : ↥H) → K)
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        0)
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)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
⊢ -(⇑α : (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)
have h₃ : -(⇑α : (a : ↥H) → K) =
  -(⇑α : (a : ↥H) → K) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (-(⇑α : (a : ↥H) → K)) +
    HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
      (⇑α : (a : ↥H) → K)
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        0)
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)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
h₃ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (-(⇑α : (a : ↥H) → K)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
⊢ -(⇑α : (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)
have h₄ : -(⇑α : (a : ↥H) → K) =
  -(⇑α : (a : ↥H) → K) +
    (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (-(⇑α : (a : ↥H) → K)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K))
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        (⇑0 : (a : ↥H) → 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)) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
        0)
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)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
h₃ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (-(⇑α : (a : ↥H) → K)) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K)
h₄ :
  -(⇑α : (a : ↥H) → K) =
    -(⇑α : (a : ↥H) → K) +
      (HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (-(⇑α : (a : ↥H) → K)) +
        HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K))
⊢ -(⇑α : (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)
have h₅ : -(⇑α : (a : ↥H) → K) =
  -(⇑α : (a : ↥H) → K) +
    (-HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
          (⇑α : (a : ↥H) → K) +
      HSMul.hSMul (β := ↥H → K) (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0)
        (⇑α : (a : ↥H) → K))
Tactic: rw [coe_chainTop', Weight.coe_zero, add_zero, succ_nsmul',
        add_assoc, smul_neg, neg_add_cancel, 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 : 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),
    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
have 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)
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]
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e 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)
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have 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
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⟩
-- 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
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
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have 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⁆
Tactic: apply_fun (⁅f, ·⁆) at hk
Cleared hypotheses: hk
-- 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
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⁆
⊢ ¬1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
have 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)
Tactic: simp only [lie_smul, lie_self, smul_zero, prim.lie_f_pow_toEnd_f] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.RootSystem (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : CharZero K
inst_2 : LieRing L
inst_3 : LieAlgebra K L
inst_4 : IsKilling K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsTriangularizable K (↥H) L
α : Weight K (↥H) L
inst_8 : Nontrivial L
hα : α.IsNonZero
x : L
hx : Membership.mem (γ := LieSubmodule K (↥H) L) (genWeightSpace L (⇑(chainTop (⇑α : (a : ↥H) → K) 0) : (a : ↥H) → K)) x
x_ne0 : x ≠ 0
e_1 f : L
he : e_1 ∈ rootSpace H (⇑α : (a : ↥H) → K)
hf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
isSl2 : IsSl2Triple (↑(coroot α) : L) e_1 f
prim : IsSl2Triple.HasPrimitiveVectorWith.{u_1, u_2, u_2} (R := K) isSl2 x (↑(chainLength α 0) : K)
k : K
hk :
  Eq (α := L) (0 : L)
    ((HPow.hPow (α := End K L) ((toEnd K L L : (a : L) → End K L) f : End K L)
            (chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1) :
          (a : L) → L)
        x :
      L)
e : 1 < chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0
⊢ False
have h₂ : chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
Tactic: refine prim.pow_toEnd_f_ne_zero_of_eq_nat rfl ?_ hk.symm
-- 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
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
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
have 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)
Tactic: have := (apply_coroot_eq_cast' α 0).symm
-- 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
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)
⊢ chainTopCoeff.{u_1, u_2, u_2} (R := K) (L := ↥H) (M := L) (⇑α : (a : ↥H) → K) 0 + 1 + 1 ≤ chainLength α 0
have this₁ : 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
Cleared hypotheses: this