-- 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
simp :
  (∃ (c₁ : K) (c₂ : K) (c₃ : K),
      x =
        c₁ •
              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)))
                        ⋯)
                      e f ∧
                    e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                ⋯ +
            c₂ •
              Classical.choose (p := fun (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)))
                      ⋯)
                    (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)))
                              ⋯)
                            e f ∧
                          e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                      ⋯)
                    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)))
                                ⋯)
                              e f ∧
                            e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                        ⋯ ∈
                      rootSpace H (⇑α : (a : ↥H) → K) ∧
                    f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                ⋯ +
          c₃ •
            ⁅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)))
                        ⋯)
                      e f ∧
                    e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                ⋯,
              Classical.choose (p := fun (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)))
                      ⋯)
                    (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)))
                              ⋯)
                            e f ∧
                          e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                      ⋯)
                    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)))
                                ⋯)
                              e f ∧
                            e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                        ⋯ ∈
                      rootSpace H (⇑α : (a : ↥H) → K) ∧
                    f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                ⋯⁆) ↔
    ∃ (c₁ : K) (c₂ : K) (c₃ : K), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
⊢ x ∈ sl2SubalgebraOfRoot hα ↔ ∃ (c₁ : K) (c₂ : K) (c₃ : K), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
simp only [sl2SubalgebraOfRoot, IsSl2Triple.mem_toLieSubalgebra_iff]

Premises used: IsSl2Triple.mem_toLieSubalgebra_iff, LieAlgebra.IsKilling.sl2SubalgebraOfRoot