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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
⊢ Eq (α := K) ((evalRingHom 0 : (a : K[X]) → K) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) : K)
    ((evalRingHom 0 : (a : K[X]) → K) 0 : K)

Tactic:
apply_fun (evalRingHom 0) at H

Premises used: Polynomial.evalRingHom, OfNat.ofNat
-- 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 :
  Eq (α := K) ((evalRingHom 0 : (a : K[X]) → K) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) : K)
    ((evalRingHom 0 : (a : K[X]) → K) 0 : K)
⊢ ∃ (m : Q),
    m ≠ 0 ∧
      Eq (α := Q)
        ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) 0 u + x') : End K Q) :
              (a : Q) → Q)
            m :
          Q)
        (0 : Q)

Tactic:
rw [constantCoeff_apply, ← coeff_map, lieCharpoly_map_eval,
        ← constantCoeff_apply, map_zero, LinearMap.charpoly_constantCoeff_eq_zero_iff] at H

Premises used: Polynomial.coeff_map, Polynomial.constantCoeff_apply, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, map_zero, LinearMap.charpoly_constantCoeff_eq_zero_iff
-- 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 :
  ∃ (m : Q),
    m ≠ 0 ∧
      Eq (α := Q)
        ((((toEnd K (↥U) Q : (a : ↥U) → End K Q) (HSMul.hSMul.{u_1, u_2, u_2} (α := K) 0 u + x') : End K Q) :
              (a : Q) → Q)
            m :
          Q)
        (0 : Q)
⊢ ∃ (z : Q), z ≠ 0 ∧ ⁅x', z⁆ = 0

Tactic:
simpa only [coe_bracket_of_module, ne_eq, zero_smul, zero_add, toEnd_apply_apply]
        using H

Premises used: LieSubalgebra.coe_bracket_of_module, zero_add, ne_eq, zero_smul, LieModule.toEnd_apply_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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
obtain : ∀ (z : Q) (hz0 : z ≠ 0) (hxz : ⁅x', z⁆ = 0), False
⊢ False

Tactic:
obtain ⟨z, hz0, hxz⟩ : ∃ z : Q, z ≠ 0 ∧ ⁅x', z⁆ = 0 := by
      -- Indeed, if the constant coefficient of `ψ` is trivial,
      -- then `0` is a root of the characteristic polynomial of `⁅0 • u + x, _⁆` acting on `Q`,
      -- and hence we find an eigenvector `z` as desired.
      apply_fun (evalRingHom 0) at H
      rw [constantCoeff_apply, ← coeff_map, lieCharpoly_map_eval,
        ← constantCoeff_apply, map_zero, LinearMap.charpoly_constantCoeff_eq_zero_iff] at H
      simpa only [coe_bracket_of_module, ne_eq, zero_smul, zero_add, toEnd_apply_apply]
        using 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : Q
hz0 : z ≠ 0
hxz : ⁅x', z⁆ = 0
apply : z = 0
⊢ False

Tactic:
apply hz0
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : Q
hz0 : z ≠ 0
hxz : ⁅x', z⁆ = 0
obtain :
  ∀ (z : L) (hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q))
    (hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)),
    Eq (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
⊢ z = 0

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

Premises used: LieSubmodule.Quotient.surjective_mk', 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
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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
rwa rwa₁ rwa₂ rwa₃ : Eq (α := L ⧸ E) (LieSubmodule.Quotient.mk ⁅x, z⁆) 0
⊢ ⁅x, z⁆ ∈ E

Tactic:
rwa [← LieSubmodule.Quotient.mk_eq_zero']

Premises used: LieSubmodule.Quotient.mk_eq_zero'
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
⊢ ⁅x, z⁆ ∈ E

Tactic:
have : ⁅x, z⁆ ∈ E := by rwa [← LieSubmodule.Quotient.mk_eq_zero']
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
this : ⁅x, z⁆ ∈ E
simp :
  ∀
    (this :
      ∃ (n : ℕ),
        Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) ⁅x, z⁆ : L)
          (0 : L)),
    ∃ (n : ℕ),
      Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) z : L) (0 : L)
⊢ Eq (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)

Tactic:
simp only [LieSubmodule.mem_mk_iff', LieSubalgebra.mem_toSubmodule, mem_engel_iff,
      LieSubmodule.Quotient.mk'_apply, LieSubmodule.Quotient.mk_eq_zero', E, Q] at this ⊢

Premises used: LieSubmodule.mem_mk_iff', LieSubalgebra.mem_toSubmodule, LieSubalgebra.mem_engel_iff, LieSubmodule.Quotient.mk_eq_zero', LieSubmodule.Quotient.mk'_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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
this :
  ∃ (n : ℕ),
    Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) ⁅x, z⁆ : L)
      (0 : L)
obtain :
  ∀ (n : ℕ)
    (hn :
      Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) ⁅x, z⁆ : L)
        (0 : L)),
    ∃ (n : ℕ),
      Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) z : L) (0 : L)
⊢ ∃ (n : ℕ),
    Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) z : L) (0 : L)

Tactic:
obtain ⟨n, hn⟩ := 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
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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
n : ℕ
hn :
  Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) ⁅x, z⁆ : L) (0 : L)
h :
  Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) (n + 1) : (a : L) → L) z : L)
    (0 : L)
⊢ ∃ (n : ℕ),
    Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) z : L) (0 : L)

Tactic:
use n + 1
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : L
hz0 : Ne (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
hxz : Eq (α := Q) (⁅x', (LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z⁆ : Q) (0 : Q)
n : ℕ
hn :
  Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n : (a : L) → L) ⁅x, z⁆ : L) (0 : L)
h h₁ h₂ h₃ :
  Eq (α := L)
    ((HMul.hMul (β := End K L) (HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) n)
            ((ad K L : (a : L) → End K L) x : End K L) :
          (a : L) → L)
        z :
      L)
    (0 : L)
⊢ Eq (α := L) ((HPow.hPow (α := End K L) ((ad K L : (a : L) → End K L) x : End K L) (n + 1) : (a : L) → L) z : L)
    (0 : L)

Tactic:
rwa [pow_succ]

Premises used: pow_succ