awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanExists
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)
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)
⊢ Eq (α := ℕ) 0 0 ∨ ∃ (k : ℕ), 0 = k + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.CartanExists
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)
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)
n_1 : ℕ
⊢ n_1 + 1 = 0 ∨ ∃ (k : ℕ), n_1 + 1 = k + 1

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.CartanExists
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)
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)
inl : ∀ (hn₀ : n = 0), z' = 0
inr : ∀ (k : ℕ) (hk : n = k + 1), z' = 0
⊢ z' = 0

Tactic:
obtain hn₀ | ⟨k, hk⟩ : n = 0 ∨ ∃ k, n = k + 1 := by cases n <;> simp
-- Module: Mathlib.Algebra.Lie.CartanExists
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)
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)
hn₀ : n = 0
⊢ z' = 0

Tactic:
simpa only [hn₀, pow_zero, Module.End.one_apply] using hn

Premises used: pow_zero, Module.End.one_apply
-- Module: Mathlib.Algebra.Lie.CartanExists
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)
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
⊢ eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0

Tactic:
specialize hsψ α hα
-- Module: Mathlib.Algebra.Lie.CartanExists
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ψ : eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
⊢ ¬∃ (m : Q),
      m ≠ 0 ∧ Eq (α := Q) ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q) m : Q) (0 : Q)

Tactic:
rw [← coe_evalRingHom, constantCoeff_apply, ← coeff_map, lieCharpoly_map_eval,
    ← constantCoeff_apply, ne_eq, LinearMap.charpoly_constantCoeff_eq_zero_iff] at hsψ

Premises used: Polynomial.coeff_map, Polynomial.constantCoeff_apply, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, ne_eq, LinearMap.charpoly_constantCoeff_eq_zero_iff, Polynomial.coe_evalRingHom
-- Module: Mathlib.Algebra.Lie.CartanExists
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ψ :
  ¬∃ (m : Q),
      m ≠ 0 ∧ Eq (α := Q) ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q) m : Q) (0 : Q)
inr :
  ∀ (hsψ : z' ≠ 0),
    ∃ (m : Q),
      m ≠ 0 ∧ Eq (α := Q) ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q) m : Q) (0 : Q)
⊢ z' = 0

Tactic:
contrapose! hsψ
-- Module: Mathlib.Algebra.Lie.CartanExists
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 :
  Ne (α := 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) ∧
    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)
⊢ ∃ (m : Q),
    m ≠ 0 ∧ Eq (α := Q) ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (α • u + x') : End K Q) : (a : Q) → Q) m : Q) (0 : Q)

Tactic:
use (toEnd K U Q v ^ k) z'

Premises used: Membership.mem, Subtype, HPow.hPow, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.CartanExists
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
⊢ Ne (α := 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) ∧
    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)

Tactic:
⟨?_, ?_⟩

Premises used: And.intro