-- 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
obtain :
  ∀ (cf : K)
    (hcf :
      hf.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)))
                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))) =
        cf • f),
    (∃ (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)))
                          pf_2)
                        e f ∧
                      e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                  he +
              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)))
                        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)))
                  hf +
            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)))
                          pf_2)
                        e f ∧
                      e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                  he,
                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)))
                        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)))
                  hf⁆) ↔
      ∃ (c₁ : K) (c₂ : K) (c₃ : K), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆
⊢ (∃ (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)))
                        pf_2)
                      e f ∧
                    e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                he +
            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)))
                      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)))
                hf +
          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)))
                        pf_2)
                      e f ∧
                    e ∈ rootSpace H (⇑α : (a : ↥H) → K) ∧ f ∈ rootSpace H (-(⇑α : (a : ↥H) → K)))
                he,
              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)))
                      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)))
                hf⁆) ↔
    ∃ (c₁ : K) (c₂ : K) (c₃ : K), x = c₁ • e + c₂ • f + c₃ • ⁅e, f⁆

Tactic:
obtain ⟨cf, hcf⟩ : ∃ c : K, hf.choose = c • f := by
    obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨f, htf⟩ (by simpa using t.f_ne_zero)).mp
      (finrank_rootSpace_eq_one (-α) (by simpa)) ⟨_, hf.choose_spec.2.2⟩
    exact ⟨c, by simpa using hc.symm⟩

Premises used: Exists.choose