-- Lean 4 proof step from Mathlib.Algebra.Lie.Weights.Killing (goal)
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))
⊢ ∃ (c : K),
    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))) =
      c • e
have obtain : ∀ (c : K)
  (hc :
    c • Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K)) e hte =
      Subtype.mk (p := fun (x : L) ↦ x ∈ rootSpace H (⇑α : (a : ↥H) → K))
        (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))))
        sorry),
  ∃ (c : K),
    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))) =
      c • e
Tactic: obtain ⟨c, hc⟩ := (finrank_eq_one_iff_of_nonzero' ⟨e, hte⟩ (by simpa using t.e_ne_zero)).mp
      (finrank_rootSpace_eq_one α hα) ⟨_, he.choose_spec.choose_spec.2.1⟩