awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
contra : 1 < finrank.{u_2, u_3} K ↥(rootSpace H (⇑α : (a : ↥H) → K))
h e f : L
ht : IsSl2Triple h e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
F : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id K) (↥(rootSpace H (⇑α : (a : ↥H) → K))) K :=
  (killingForm K L : (a : L) → L →ₗ[K] K) f ∘ₗ (↑(rootSpace H (⇑α : (a : ↥H) → K)) : Submodule K L).subtype
hF : F.ker ≠ ⊥
y : L
hyα : y ∈ rootSpace H (⇑α : (a : ↥H) → K)
hy₀ : Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) y hyα ≠ 0
hy : ⁅y, f⁆ = 0
P : IsSl2Triple.HasPrimitiveVectorWith.{u_2, u_3, u_3} (R := K) ⋯ y (-2)
n : ℕ
hn : Eq.{u_2 + 1} (α := K) (-2) (↑n : K)
assumption_mod_cast assumption_mod_cast₁ assumption_mod_cast₂ assumption_mod_cast₃ :
  ∀ (P : IsSl2Triple.HasPrimitiveVectorWith.{u_2, u_3, u_3} (R := K) ⋯ y (↑(Int.negSucc 1) : K)) (hn : False), False
⊢ False

Tactic:
assumption_mod_cast
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
choose :
  (h e f : L) →
    (t : IsSl2Triple h e f) →
      (ht : e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))) → LieSubalgebra K L
⊢ LieSubalgebra K L

Tactic:
choose h e f t ht using exists_isSl2Triple_of_weight_isNonZero hα

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
ht : e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ LieSubalgebra K L

Tactic:
exact t.toLieSubalgebra K

Premises used: IsSl2Triple.toLieSubalgebra
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
htf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
x : L
pf : LieRing.IsNilpotent.{u_3} ↥H
pf_1 : LieModule K (↥H) L
pf_2 :
  ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
he :
  ∃ (e : L) (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        e f ∧
      e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf :
  ∃ (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        (Classical.choose (p := fun (e : L) ↦
          ∃ (f : L),
            IsSl2Triple
                (Classical.choose (p := fun (h : L) ↦
                  ∃ (e : L) (f : L),
                    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                  pf_2)
                e f ∧
              e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          he)
        f ∧
      Classical.choose (p := fun (e : L) ↦
            ∃ (f : L),
              IsSl2Triple
                  (Classical.choose (p := fun (h : L) ↦
                    ∃ (e : L) (f : L),
                      IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                    pf_2)
                  e f ∧
                e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
            he ∈
          rootSpace H (⇑α : (a : ↥H) → K) ∧
        f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) e hte ≠ 0

Tactic:
simpa using t.e_ne_zero

Premises used: IsSl2Triple.e_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
htf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
x : L
pf : LieRing.IsNilpotent.{u_3} ↥H
pf_1 : LieModule K (↥H) L
pf_2 :
  ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
he :
  ∃ (e : L) (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        e f ∧
      e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf :
  ∃ (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        (Classical.choose (p := fun (e : L) ↦
          ∃ (f : L),
            IsSl2Triple
                (Classical.choose (p := fun (h : L) ↦
                  ∃ (e : L) (f : L),
                    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                  pf_2)
                e f ∧
              e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          he)
        f ∧
      Classical.choose (p := fun (e : L) ↦
            ∃ (f : L),
              IsSl2Triple
                  (Classical.choose (p := fun (h : L) ↦
                    ∃ (e : L) (f : L),
                      IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                    pf_2)
                  e f ∧
                e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
            he ∈
          rootSpace H (⇑α : (a : ↥H) → K) ∧
        f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
ce : K
hce :
  he.choose (p := fun (e : L) ↦
      ∃ (f : L),
        IsSl2Triple
            (Classical.choose (p := fun (h : L) ↦
              ∃ (e : L) (f : L),
                IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
              pf_2)
            e f ∧
          e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))) =
    ce • e
⊢ Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑(-α) : (a : ↥H) → K)) f htf ≠ 0

Tactic:
simpa using t.f_ne_zero

Premises used: IsSl2Triple.f_ne_zero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
K : Type u_2
L : Type u_3
inst : LieRing L
inst_1 : Field K
inst_2 : LieAlgebra K L
inst_3 : FiniteDimensional K L
H : LieSubalgebra K L
inst_4 : H.IsCartanSubalgebra
inst_5 : IsKilling K L
inst_6 : IsTriangularizable K (↥H) L
inst_7 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h e f : L
t : IsSl2Triple h e f
hte : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
htf : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
x : L
pf : LieRing.IsNilpotent.{u_3} ↥H
pf_1 : LieModule K (↥H) L
pf_2 :
  ∃ (h : L) (e : L) (f : L),
    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
he :
  ∃ (e : L) (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        e f ∧
      e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hf :
  ∃ (f : L),
    IsSl2Triple
        (Classical.choose (p := fun (h : L) ↦
          ∃ (e : L) (f : L),
            IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          pf_2)
        (Classical.choose (p := fun (e : L) ↦
          ∃ (f : L),
            IsSl2Triple
                (Classical.choose (p := fun (h : L) ↦
                  ∃ (e : L) (f : L),
                    IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                  pf_2)
                e f ∧
              e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
          he)
        f ∧
      Classical.choose (p := fun (e : L) ↦
            ∃ (f : L),
              IsSl2Triple
                  (Classical.choose (p := fun (h : L) ↦
                    ∃ (e : L) (f : L),
                      IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                    pf_2)
                  e f ∧
                e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
            he ∈
          rootSpace H (⇑α : (a : ↥H) → K) ∧
        f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
ce : K
hce :
  he.choose (p := fun (e : L) ↦
      ∃ (f : L),
        IsSl2Triple
            (Classical.choose (p := fun (h : L) ↦
              ∃ (e : L) (f : L),
                IsSl2Triple h e f ∧ e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
              pf_2)
            e f ∧
          e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))) =
    ce • e
⊢ (-α).IsNonZero

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
x : L
hx : x ∈ (sl2SubalgebraOfRoot hα).carrier
this : ⁅(↑h : L), x⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅h, x⁆ ∈ (sl2SubalgebraOfRoot hα).carrier

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
x : L
hx : x ∈ (sl2SubalgebraOfRoot hα).carrier
suffices : ⁅(↑h : L), x⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅h, x⁆ ∈ (sl2SubalgebraOfRoot hα).carrier

Tactic:
suffices ⁅(h : L), x⁆ ∈ sl2SubalgebraOfRoot hα by simpa
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
x : L
hx : x ∈ (sl2SubalgebraOfRoot hα).carrier
obtain :
  ∀ (h' e f : L) (ht : IsSl2Triple h' e f) (heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K))
    (hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))), ⁅(↑h : L), x⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅(↑h : L), x⁆ ∈ sl2SubalgebraOfRoot hα

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

Premises used: LieAlgebra.IsKilling.exists_isSl2Triple_of_weight_isNonZero
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
x : L
hx : x ∈ (sl2SubalgebraOfRoot hα).carrier
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
⊢ x ∈ sl2SubalgebraOfRoot hα

Tactic:
replace hx : x ∈ sl2SubalgebraOfRoot hα := hx
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
x h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
hx : x ∈ sl2SubalgebraOfRoot hα
obtain :
  ∀ (c₁ c₂ c₃ : K) (hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα),
    ⁅(↑h : L), c₁ • e + c₂ • f + c₃ • ⁅e, f⁆⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅(↑h : L), x⁆ ∈ sl2SubalgebraOfRoot hα

Tactic:
obtain ⟨c₁, c₂, c₃, rfl⟩ := (mem_sl2SubalgebraOfRoot_iff hα ht heα hfα).mp hx

Premises used: Iff.mp, LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, rfl
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
rw :
  ∃ (c₁_1 : K) (c₂_1 : K) (c₃_1 : K),
    c₁ • ⁅(↑h : L), e⁆ + c₂ • ⁅(↑h : L), f⁆ + c₃ • ⁅(↑h : L), ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆
⊢ ⁅(↑h : L), c₁ • e + c₂ • f + c₃ • ⁅e, f⁆⁆ ∈ sl2SubalgebraOfRoot hα

Tactic:
rw [mem_sl2SubalgebraOfRoot_iff hα ht heα hfα, lie_add, lie_add, lie_smul, lie_smul, lie_smul]

Premises used: lie_smul, LieAlgebra.IsKilling.mem_sl2SubalgebraOfRoot_iff, lie_add
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
⊢ ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e

Tactic:
have he_wt : ⁅(h : L), e⁆ = α h • e := lie_eq_smul_of_mem_rootSpace heα h
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
⊢ ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f

Tactic:
have hf_wt : ⁅(h : L), f⁆ = (-α) h • f := lie_eq_smul_of_mem_rootSpace hfα h
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
suffices : ⁅e, f⁆ ∈ rootSpace H 0
⊢ ⁅(↑h : L), ⁅e, f⁆⁆ = 0

Tactic:
suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
        lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
rw : (↑(coroot α) : L) ∈ H.toLieSubmodule
⊢ ⁅e, f⁆ ∈ rootSpace H 0

Tactic:
rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]

Premises used: IsSl2Triple.h_eq_coroot, LieAlgebra.rootSpace_zero_eq, IsSl2Triple.lie_e_f
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ (↑(coroot α) : L) ∈ H.toLieSubmodule

Tactic:
(coroot α).property

Premises used: Set.Mem, LieAlgebra.IsKilling.coroot, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ (↑(coroot α) : L) ∈ H.toLieSubmodule

Tactic:
exact (coroot α).property

Premises used: LieAlgebra.IsKilling.coroot, Subtype.property
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
⊢ ⁅(↑h : L), ⁅e, f⁆⁆ = 0

Tactic:
have hef_zero : ⁅(h : L), ⁅e, f⁆⁆ = 0 := by
      suffices h_coroot_in_zero : ⁅e, f⁆ ∈ rootSpace H (0 : H → K) from
        lie_eq_smul_of_mem_rootSpace h_coroot_in_zero h ▸ (zero_smul K ⁅e, f⁆)
      rw [ht.lie_e_f, IsSl2Triple.h_eq_coroot hα ht heα hfα, rootSpace_zero_eq K L H]
      exact (coroot α).property
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
hef_zero : ⁅(↑h : L), ⁅e, f⁆⁆ = 0
⊢ c₁ • ⁅(↑h : L), e⁆ + c₂ • ⁅(↑h : L), f⁆ + c₃ • ⁅(↑h : L), ⁅e, f⁆⁆ =
    HMul.hMul (β := K) c₁ ((α : (a : ↥H) → K) h : K) • e + HMul.hMul (β := K) c₂ (-(α : (a : ↥H) → K) h : K) • f +
      HSMul.hSMul.{u_2, u_3, u_3} (α := K) 0 ⁅e, f⁆

Tactic:
simp [he_wt, hf_wt, hef_zero, smul_smul]

Premises used: smul_smul
-- Module: Mathlib.Algebra.Lie.Weights.Killing
Goal:
R : Type u_1
K : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : Field K
inst_4 : LieAlgebra K L
inst_5 : FiniteDimensional K L
H : LieSubalgebra K L
inst_6 : H.IsCartanSubalgebra
inst_7 : IsKilling K L
inst_8 : IsTriangularizable K (↥H) L
inst_9 : CharZero K
α : Weight K (↥H) L
hα : α.IsNonZero
h : ↥H
h' e f : L
ht : IsSl2Triple h' e f
heα : e ∈ rootSpace H (⇑α : (a : ↥H) → K)
hfα : f ∈ rootSpace H (-(⇑α : (a : ↥H) → K))
c₁ c₂ c₃ : K
hx : c₁ • e + c₂ • f + c₃ • ⁅e, f⁆ ∈ sl2SubalgebraOfRoot hα
he_wt : ⁅(↑h : L), e⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((α : (a : ↥H) → K) h : K) e
hf_wt : ⁅(↑h : L), f⁆ = HSMul.hSMul.{u_2, u_3, u_3} (α := K) ((-α : (a : ↥H) → K) h : K) f
hef_zero : ⁅(↑h : L), ⁅e, f⁆⁆ = 0
⊢ ∃ (c₁_1 : K) (c₂_1 : K) (c₃_1 : K),
    c₁ • ⁅(↑h : L), e⁆ + c₂ • ⁅(↑h : L), f⁆ + c₃ • ⁅(↑h : L), ⁅e, f⁆⁆ = c₁_1 • e + c₂_1 • f + c₃_1 • ⁅e, f⁆

Tactic:
exact ⟨c₁ * α h, c₂ * (-α h), 0, by simp [he_wt, hf_wt, hef_zero, smul_smul]⟩