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
α : 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)
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)
    (0 : Q)
⊢ 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:
refine ⟨?_, ?_⟩
-- 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 :
  k <
    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'
⊢ 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)

Tactic:
apply Nat.find_min hz'

Premises used: Nat.find_min
-- 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
⊢ k <
    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'

Tactic:
lia
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
obtain : ∀ (x : L) (hx : IsRegular K x), ∃ (x : L), IsCartanSubalgebra (engel K x)
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)

Tactic:
obtain ⟨x, hx⟩ := exists_isRegular_of_finrank_le_card K L h

Premises used: LieAlgebra.exists_isRegular_of_finrank_le_card
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
h₁ : IsCartanSubalgebra (engel K x)
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)

Tactic:
use x
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
⊢ IsCartanSubalgebra (engel K x)

Tactic:
⟨?_, normalizer_engel _ _⟩

Premises used: LieSubalgebra.normalizer_engel, LieSubalgebra.IsCartanSubalgebra.mk
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
h₁ : LieRing.IsNilpotent.{u_2} ↥(engel K x)
⊢ IsCartanSubalgebra (engel K x)

Tactic:
refine ⟨?_, normalizer_engel _ _⟩
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
h₁ :
  ∀ (x_1 : L),
    Membership.mem (γ := LieSubalgebra K L) (engel K x) x_1 → LE.le (α := LieSubalgebra K L) (engel K x) (engel K x_1)
⊢ LieRing.IsNilpotent.{u_2} ↥(engel K x)

Tactic:
apply isNilpotent_of_forall_le_engel

Premises used: LieSubalgebra.isNilpotent_of_forall_le_engel
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
h₁ : IsBot Ex
⊢ LE.le (α := LieSubalgebra K L) (engel K x) (engel K y)

Tactic:
suffices IsBot Ex from @this ⟨engel K y, y, hy, rfl⟩
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
h₁ : IsMin Ex
⊢ IsBot Ex

Tactic:
apply engel_isBot_of_isMin h (engel K x) Ex le_rfl

Premises used: le_rfl, LieSubalgebra.engel, LieAlgebra.engel_isBot_of_isMin
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
suffices : Eq (α := LieSubalgebra K L) (engel K y) (engel K x)
⊢ Ex ≤
    Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯

Tactic:
suffices engel K y = engel K x from this.ge
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
a : Eq (α := Submodule K L) (LieSubalgebra.toSubmodule (engel K y)) (LieSubalgebra.toSubmodule (engel K x))
⊢ Eq (α := LieSubalgebra K L) (engel K y) (engel K x)

Tactic:
apply LieSubalgebra.toSubmodule_injective

Premises used: LieSubalgebra.toSubmodule_injective
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ Eq (α := Submodule K L) (LieSubalgebra.toSubmodule (engel K y)) (LieSubalgebra.toSubmodule (engel K x))

Tactic:
Submodule.eq_of_le_of_finrank_le hyx this

Premises used: Submodule.eq_of_le_of_finrank_le
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
this : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ Eq (α := Submodule K L) (LieSubalgebra.toSubmodule (engel K y)) (LieSubalgebra.toSubmodule (engel K x))

Tactic:
exact Submodule.eq_of_le_of_finrank_le hyx this

Premises used: Submodule.eq_of_le_of_finrank_le
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
h₁ : finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ Ex ≤
    Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯

Tactic:
suffices finrank K (engel K x) ≤ finrank K (engel K y) by
    suffices engel K y = engel K x from this.ge
    apply LieSubalgebra.toSubmodule_injective
    exact Submodule.eq_of_le_of_finrank_le hyx this
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
h₁ : rank K L ≤ finrank.{u_1, u_2} K ↥(engel K y)
⊢ finrank.{u_1, u_2} K ↥(engel K x) ≤ finrank.{u_1, u_2} K ↥(engel K y)

Tactic:
rw [(isRegular_iff_finrank_engel_eq_rank K x).mp hx]

Premises used: Iff.mp, LieAlgebra.isRegular_iff_finrank_engel_eq_rank
-- 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
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
x : L
hx : IsRegular K x
y_1 : L
hy_1 : Membership.mem (γ := LieSubalgebra K L) (engel K x) y_1
Ex : (↑{x_1 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_1} :
  Type u_2) :=
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
    Membership.mem (γ := Set (LieSubalgebra K L))
      {x_2 : LieSubalgebra K L | ∃ (z : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) z ∧ engel K z = x_2}
      x_1)
    (engel K x) ⋯
y : L
hy : Membership.mem (γ := LieSubalgebra K L) (engel K x) y
hyx :
  Subtype.mk (p := fun (x_1 : LieSubalgebra K L) ↦
      Membership.mem (γ := Set (LieSubalgebra K L))
        {x_2 : LieSubalgebra K L |
          ∃ (x_3 : L), Membership.mem (γ := LieSubalgebra K L) (engel K x) x_3 ∧ engel K x_3 = x_2}
        x_1)
      (engel K y) ⋯ ≤
    Ex
⊢ rank K L ≤ finrank.{u_1, u_2} K ↥(engel K y)

Tactic:
apply rank_le_finrank_engel

Premises used: LieAlgebra.rank_le_finrank_engel
-- 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
inst_4 : Infinite K
h : (↑(finrank K L) : Cardinal.{u_1}) ≤ #K
⊢ ∃ (x : L), IsCartanSubalgebra (engel K x)

Tactic:
apply exists_isCartanSubalgebra_engel_of_finrank_le_card

Premises used: LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card
-- 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
inst_4 : Infinite K
⊢ (↑(finrank K L) : Cardinal.{u_1}) ≤ #K

Tactic:
natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite K›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- 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
inst_4 : Infinite K
⊢ (↑(finrank K L) : Cardinal.{u_1}) ≤ #K

Tactic:
exact natCast_le_aleph0.trans <| Cardinal.infinite_iff.mp ‹Infinite K›

Premises used: Cardinal.infinite_iff, Iff.mp, LE.le.trans, Cardinal.natCast_le_aleph0
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
⊢ LieRing.IsNilpotent.{v} ↥H

Tactic:
IsCartanSubalgebra.nilpotent

Premises used: LieSubalgebra.IsCartanSubalgebra.nilpotent
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
rw : (↑H.toLieSubmodule.normalizer : Submodule R L) = (↑H.toLieSubmodule : Submodule R L)
rw₁ : H.normalizer.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
rw₂ : H.toSubmodule = (↑H.toLieSubmodule : Submodule R L)
rw₃ rw₄ : H.toSubmodule = H.toSubmodule
⊢ H.toLieSubmodule.normalizer = H.toLieSubmodule

Tactic:
rw [← LieSubmodule.toSubmodule_inj, coe_normalizer_eq_normalizer,
    IsCartanSubalgebra.self_normalizing, coe_toLieSubmodule]

Premises used: LieSubalgebra.coe_normalizer_eq_normalizer, LieSubmodule.toSubmodule_inj, LieSubalgebra.coe_toLieSubmodule, LieSubalgebra.IsCartanSubalgebra.self_normalizing
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
⊢ LieSubmodule.ucs 0 H.toLieSubmodule = H.toLieSubmodule

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.CartanSubalgebra
Goal:
R : Type u
L : Type v
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
H : LieSubalgebra R L
inst_3 : H.IsCartanSubalgebra
k : ℕ
ih : LieSubmodule.ucs k H.toLieSubmodule = H.toLieSubmodule
⊢ LieSubmodule.ucs (k + 1) H.toLieSubmodule = H.toLieSubmodule

Tactic:
simp [ih]