-- Mathlib/Algebra/Lie/CartanExists.lean
/-- Let `L` be a Lie algebra of dimension `n` over a field `K` with at least `n` elements.
Given a Lie subalgebra `U` of `L`, and an element `x ∈ U` such that `U ≤ engel K x`.
Suppose that `engel K x` is minimal amongst the Engel subalgebras `engel K y` for `y ∈ U`.
Then `engel K x ≤ engel K y` for all `y ∈ U`.

Lemma 2 in [barnes1967]. -/
lemma engel_isBot_of_isMin (hLK : finrank K L ≤ #K) (U : LieSubalgebra K L)
    (E : {engel K x | x ∈ U}) (hUle : U ≤ E) (hmin : IsMin E) :
    IsBot E

Proof state:
case inr.refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ((toEnd K ↥U ↥E) (α • u + x')) ⟨↑z, ⋯⟩ = 0

Tactic:
show ⁅z, _⁆ = (0 : E)

Result:
case inr.refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ⁅z, ⟨↑z, ⋯⟩⁆ = 0

Proof state:
case intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
H : constantCoeff ψ = 0
z : Q
hz0 : z ≠ 0
hxz : ⁅x', z⁆ = 0
⊢ z = 0

Tactic:
obtain ⟨z, rfl⟩ := LieSubmodule.Quotient.surjective_mk' E z

Result:
case intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
H : constantCoeff ψ = 0
z : L
hz0 : (LieSubmodule.Quotient.mk' E) z ≠ 0
hxz : ⁅x', (LieSubmodule.Quotient.mk' E) z⁆ = 0
⊢ (LieSubmodule.Quotient.mk' E) z = 0

Proof state:
case h.refine_2
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : constantCoeff ψ ≠ 0
t : Finset K := (constantCoeff ψ).roots.toFinset
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
α : K
hα : α ∈ s ∧ (constantCoeff ψ ≠ 0 → ¬eval α (constantCoeff ψ) = 0)
⊢ eval α (constantCoeff ψ) ≠ 0

Tactic:
exact hα.2 hψ

Result:
no goals

Proof state:
case intro.intro.intro.intro
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
H : constantCoeff ψ = 0
z : L
hz0 : (LieSubmodule.Quotient.mk' E) z ≠ 0
hxz : ⁅x', (LieSubmodule.Quotient.mk' E) z⁆ = 0
n : ℕ
hn : ((ad K L) x ^ n) ⁅x, z⁆ = 0
⊢ ∃ n, ((ad K L) x ^ n) z = 0

Tactic:
use n+1

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
hLK : ↑(finrank K L) ≤ #K
U : LieSubalgebra K L
x : L
hxU : x ∈ U
y : L
hyU : y ∈ U
Ex : ↑{x | ∃ x_1 ∈ U, engel K x_1 = x} := ⟨engel K x, ⋯⟩
Ey : ↑{x | ∃ y ∈ U, engel K y = x} := ⟨engel K y, ⋯⟩
hUle : U ≤ ↑Ex
hmin : ∀ E ≤ Ex, Ex ≤ E
E : LieSubmodule K (↥U) L :=
  let __src := engel K x;
  { toSubmodule := __src.toSubmodule, lie_mem := ⋯ }
hx₀ : x ≠ 0
Q : Type u_2 := L ⧸ E
r : ℕ := finrank K ↥E
hr : r < finrank K L
x' : ↥U := ⟨x, hxU⟩
y' : ↥U := ⟨y, hyU⟩
u : ↥U := y' - x'
χ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K (↥E) x' u
ψ : K[X][X] := LieAlgebra.engel_isBot_of_isMin.lieCharpoly K Q x' u
i : ℕ
hi : i < r
hi0 : i ≠ 0
H : constantCoeff ψ = 0
z : L
hz0 : (LieSubmodule.Quotient.mk' E) z ≠ 0
hxz : ⁅x', (LieSubmodule.Quotient.mk' E) z⁆ = 0
n : ℕ
hn : ((ad K L) x ^ n) ⁅x, z⁆ = 0
⊢ ((ad K L) x ^ (n + 1)) z = 0