-- 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
α : 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)
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)
k : ℕ
hk : n = k + 1
hsψ : z' ≠ 0
h :
  Eq (α := Q)
    ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
      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)
h₁ :
  Eq (α := Q)
    ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
      Q)
    ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) (k + 1) : (a : Q) → Q) z' : Q)
⊢ Eq (α := Q)
    ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
        ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
      Q)
    (0 : Q)
have h₂ : Eq (α := Q)
  ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q)
      ((HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k : (a : Q) → Q) z') :
    Q)
  ((HMul.hMul (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q)
          (HPow.hPow (α := End K Q) ((toEnd K (↥U) Q : (a : ↥U) → End K Q) v : End K Q) k) :
        (a : Q) → Q)
      z' :
    Q)
Tactic: rw [← hn, hk, pow_succ', Module.End.mul_apply]