-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (goal)
Goal:
K : Type u_1
L : Type u_2
inst : Field K
inst_1 : LieRing L
inst_2 : LieAlgebra K L
inst_3 : Module.Finite K L
hLK : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : (↑{x : LieSubalgebra K L | ∃ x_1 ∈ U, engel K x_1 = x} : Type u_2) :=
  Subtype.mk (p := fun (x : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L)) {x : LieSubalgebra K L | ∃ x_1 ∈ U, engel K x_1 = x} x) (engel K x) ⋯
Ey : (↑{x : LieSubalgebra K L | ∃ y ∈ U, engel K y = x} : Type u_2) :=
  Subtype.mk (p := fun (x : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L)) {x : LieSubalgebra K L | ∃ y ∈ U, engel K y = x} x) (engel K y) ⋯
hUle : U ≤ (↑Ex : LieSubalgebra K L)
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src : LieSubalgebra K L := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank.{u_1, u_2} K ↥E
hr : r < finrank K L
x' : ↥U := Subtype.mk (p := fun (x : L) ↦ x ∈ U) x hxU
y' : ↥U := Subtype.mk (p := fun (x : L) ↦ x ∈ U) y hyU
u : ↥U := y' - x'
χ : K[X][X] := lieCharpoly K (↥E) x' u
ψ : K[X][X] := lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
s : Finset K
hs : r ≤ s.card
hsψ : ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
α : K
hα : α ∈ s
v : ↥U := α • u + x'
z : L
hz : Membership.mem (γ := LieSubalgebra K L) (engel K (↑v : L)) z
z' : Q := (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z
hz' :
  ∃ (n : ℕ),
    Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
      (0 : Q)
Now Now₁ : z' = 0
Now₂ :
  let n :=
    Nat.find (p := fun (n : ℕ) ↦
      Eq (α := Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q) (0 : Q))
      hz';
  ∀
    (_hn :
      n =
        Nat.find (p := fun (n : ℕ) ↦
          Eq (α := Q)
            ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
            (0 : Q))
          hz'),
    z' = 0
⊢ z' = 0
have Now₃ : let n :=
  Nat.find (p := fun (n : ℕ) ↦
    Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
      (0 : Q))
    hz';
∀
  (_hn :
    n =
      Nat.find (p := fun (n : ℕ) ↦
        Eq (α := Q)
          ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
          (0 : Q))
        hz')
  (hn :
    Eq (α := Q) ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) n : (a : Q) → Q) z' : Q)
      (0 : Q)),
  z' = 0
Tactic: classical
  -- Now let `n` be the smallest power such that `⁅v, _⁆ ^ n` kills `z'`.
  set n := Nat.find hz' with _hn
  have hn : (toEnd K U Q v ^ n) z' = 0 := Nat.find_spec hz'
  -- If `n = 0`, then we are done.
  obtain hn₀ | ⟨k, hk⟩ : n = 0 ∨ ∃ k, n = k + 1 := by cases n <;> simp
  · simpa only [hn₀, pow_zero, Module.End.one_apply] using hn
  -- If `n = k + 1`, then we can write `⁅v, _⁆ ^ n = ⁅v, _⁆ ∘ ⁅v, _⁆ ^ k`.
  -- Recall that `constantCoeff ψ` is non-zero on `α`, and `v = α • u + x`.
  specialize hsψ α hα
  -- Hence `⁅v, _⁆` acts injectively on `Q`.
  rw [← coe_evalRingHom, constantCoeff_apply, ← coeff_map, lieCharpoly_map_eval,
    ← constantCoeff_apply, ne_eq, LinearMap.charpoly_constantCoeff_eq_zero_iff] at hsψ
  -- We deduce from this that `z' = 0`, arguing by contraposition.
  contrapose! hsψ
  -- Indeed `⁅v, _⁆` kills `⁅v, _⁆ ^ k` applied to `z'`.
  use (toEnd K U Q v ^ k) z'
  refine ⟨?_, ?_⟩
  · -- And `⁅v, _⁆ ^ k` applied to `z'` is non-zero by definition of `n`.
    apply Nat.find_min hz'; lia
  · rw [← hn, hk, pow_succ', Module.End.mul_apply]