awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ∃ (m : ↥E),
    m ≠ 0 ∧
      Eq (α := ↥E)
        (((((toEnd.{u_1, u_2, u_2} K ↥U ↥E : ↥U →ₗ⁅K⁆ End K ↥E) : (a : ↥U) → End K ↥E) (α • u + x') : End K ↥E) :
              (a : ↥E) → ↥E)
            m :
          ↥E)
        (0 : ↥E)
have inr : Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) sorry ≠ 0
Tactic: refine ⟨⟨z, hUle z.2⟩, ?_, ?_⟩
-- 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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
inr : Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) ⋯ ≠ 0
⊢ ∃ (m : ↥E),
    m ≠ 0 ∧
      Eq (α := ↥E)
        (((((toEnd.{u_1, u_2, u_2} K ↥U ↥E : ↥U →ₗ⁅K⁆ End K ↥E) : (a : ↥U) → End K ↥E) (α • u + x') : End K ↥E) :
              (a : ↥E) → ↥E)
            m :
          ↥E)
        (0 : ↥E)
have inr₁ : Eq (α := ↥E)
  (((((toEnd.{u_1, u_2, u_2} K ↥U ↥E : ↥U →ₗ⁅K⁆ End K ↥E) : (a : ↥U) → End K ↥E) (α • u + x') : End K ↥E) :
        (a : ↥E) → ↥E)
      (Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) sorry) :
    ↥E)
  (0 : ↥E)
Tactic: refine ⟨⟨z, hUle z.2⟩, ?_, ?_⟩
-- 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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ Eq (α := ↥E)
    (((((toEnd.{u_1, u_2, u_2} K ↥U ↥E : ↥U →ₗ⁅K⁆ End K ↥E) : (a : ↥U) → End K ↥E) (α • u + x') : End K ↥E) :
          (a : ↥E) → ↥E)
        (Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) ⋯) :
      ↥E)
    (0 : ↥E)
have inr : ⁅z, Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) sorry⁆ = 0
Tactic: change ⁅z, _⁆ = (0 : E)
-- 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
hi : 0 < r
α : K
z : ↥U := α • u + x'
hz₀ : z ≠ 0
⊢ ⁅z, Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) ⋯⁆ = 0
have inr : (↑⁅z, Subtype.mk (p := fun (x : L) ↦ x ∈ E) (↑z : L) sorry⁆ : L) = (↑0 : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (hypothesis)
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), z ≠ 0 ∧ ⁅x', z⁆ = 0
have 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)
Tactic: apply_fun (evalRingHom 0) at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (hypothesis)
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)
⊢ ∃ (z : Q), z ≠ 0 ∧ ⁅x', z⁆ = 0
have 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)
Tactic: rw [constantCoeff_apply, ← coeff_map, lieCharpoly_map_eval,
        ← constantCoeff_apply, map_zero, LinearMap.charpoly_constantCoeff_eq_zero_iff] at H
Cleared hypotheses: H
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
⊢ False
have obtain : ∀ (z : Q) (hz0 : z ≠ 0) (hxz : ⁅x', z⁆ = 0), 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
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : Q
hz0 : z ≠ 0
hxz : ⁅x', z⁆ = 0
⊢ False
have apply : z = 0
Tactic: apply hz0
-- 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 : Eq (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
z : Q
hz0 : z ≠ 0
hxz : ⁅x', z⁆ = 0
⊢ z = 0
have 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)
Tactic: obtain ⟨z, rfl⟩ := LieSubmodule.Quotient.surjective_mk' E z
Cleared hypotheses: z, hz0, hxz
-- 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 : 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
have rwa : Eq (α := L ⧸ E) (LieSubmodule.Quotient.mk ⁅x, z⁆) 0
Tactic: rwa [← LieSubmodule.Quotient.mk_eq_zero']
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanExists (hypothesis)
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)
⊢ Eq (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
have this : ⁅x, z⁆ ∈ E
Tactic: have : ⁅x, z⁆ ∈ E := by rwa [← LieSubmodule.Quotient.mk_eq_zero']
-- 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 : 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
⊢ Eq (α := Q) ((LieSubmodule.Quotient.mk' E : (a : L) → L ⧸ E) z : L ⧸ E) (0 : Q)
have 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)
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 ⊢
Cleared hypotheses: this
-- 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 : 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)
⊢ ∃ (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)
have 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)
Tactic: obtain ⟨n, hn⟩ := this
Cleared hypotheses: this