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
i : ℕ
hi : i < r
hi0 : i ≠ 0
hψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ))
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have h : r ≤ (s \ t).card ∧ ∀ α ∈ s \ t, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
Tactic: use s \ t
-- 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ))
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ (s \ t).card ∧ ∀ α ∈ s \ t, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have h : r ≤ (s \ t).card
Tactic: refine ⟨?_, ?_⟩
-- 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ))
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
h : r ≤ (s \ t).card
⊢ r ≤ (s \ t).card ∧ ∀ α ∈ s \ t, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have h₁ : ∀ α ∈ s \ t, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
Tactic: refine ⟨?_, ?_⟩
-- 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ))
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
⊢ r ≤ (s \ t).card
have h : r ≤ s.card - t.card
Tactic: refine le_trans ?_ (Finset.le_card_sdiff _ _)
-- 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ))
ht : t.card ≤ finrank K L - r
s : Finset K
hs : finrank K L ≤ s.card
α : K
hα : α ∈ s \ t
⊢ eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have hα₁ : α ∈ s ∧
  (Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X]) →
    ¬eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) = 0)
Tactic: simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
Let Let₁ Let₂ : ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
⊢ ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have Let₃ : let t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ));
∀ (ht : t.card ≤ finrank K L - r),
  ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
Tactic: classical
    -- Let `t` denote the set of roots of `constantCoeff ψ`.
    let t := (constantCoeff ψ).roots.toFinset
    -- We show that `t` has cardinality at most `finrank K L - r`.
    have ht : t.card ≤ finrank K L - r := by
      refine (Multiset.toFinset_card_le _).trans ?_
      refine (card_roots' _).trans ?_
      rw [constantCoeff_apply]
      -- Indeed, `constantCoeff ψ` has degree at most `finrank K Q = finrank K L - r`.
      apply lieCharpoly_coeff_natDegree
      suffices finrank K Q + r = finrank K L by rw [← this, zero_add, Nat.add_sub_cancel]
      apply Submodule.finrank_quotient_add_finrank
    -- Hence there exists a subset of size `≥ r` in the complement of `t`,
    -- and `constantCoeff ψ` takes non-zero values on all of this subset.
    obtain ⟨s, hs⟩ := exists_finset_le_card K _ hLK
    use s \ t
    refine ⟨?_, ?_⟩
    · refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega
    · intro α hα
      simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
      exact hα.2 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
Let Let₁ Let₂ : ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
Let₃ :
  let t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ));
  ∀ (ht : t.card ≤ finrank K L - r),
    ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
⊢ ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
have Let₄ : let t : Finset K := Multiset.toFinset (roots ((constantCoeff : (a : K[X][X]) → K[X]) ψ));
∀ (ht : t.card ≤ finrank K L - r) (s : Finset K) (hs : finrank K L ≤ s.card),
  ∃ (s : Finset K), r ≤ s.card ∧ ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0
Tactic: classical
    -- Let `t` denote the set of roots of `constantCoeff ψ`.
    let t := (constantCoeff ψ).roots.toFinset
    -- We show that `t` has cardinality at most `finrank K L - r`.
    have ht : t.card ≤ finrank K L - r := by
      refine (Multiset.toFinset_card_le _).trans ?_
      refine (card_roots' _).trans ?_
      rw [constantCoeff_apply]
      -- Indeed, `constantCoeff ψ` has degree at most `finrank K Q = finrank K L - r`.
      apply lieCharpoly_coeff_natDegree
      suffices finrank K Q + r = finrank K L by rw [← this, zero_add, Nat.add_sub_cancel]
      apply Submodule.finrank_quotient_add_finrank
    -- Hence there exists a subset of size `≥ r` in the complement of `t`,
    -- and `constantCoeff ψ` takes non-zero values on all of this subset.
    obtain ⟨s, hs⟩ := exists_finset_le_card K _ hLK
    use s \ t
    refine ⟨?_, ?_⟩
    · refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega
    · intro α hα
      simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
      exact hα.2 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ψ : Ne (α := K[X]) ((constantCoeff : (a : K[X][X]) → K[X]) ψ : K[X]) (0 : K[X])
⊢ χ.coeff i = 0
have inr : ∀ (s : Finset K) (hs : r ≤ s.card) (hsψ : ∀ α ∈ s, eval α ((constantCoeff : (a : K[X][X]) → K[X]) ψ) ≠ 0), χ.coeff i = 0
Tactic: obtain ⟨s, hs, hsψ⟩ : ∃ s : Finset K, r ≤ s.card ∧ ∀ α ∈ s, (constantCoeff ψ).eval α ≠ 0 := by
    classical
    -- Let `t` denote the set of roots of `constantCoeff ψ`.
    let t := (constantCoeff ψ).roots.toFinset
    -- We show that `t` has cardinality at most `finrank K L - r`.
    have ht : t.card ≤ finrank K L - r := by
      refine (Multiset.toFinset_card_le _).trans ?_
      refine (card_roots' _).trans ?_
      rw [constantCoeff_apply]
      -- Indeed, `constantCoeff ψ` has degree at most `finrank K Q = finrank K L - r`.
      apply lieCharpoly_coeff_natDegree
      suffices finrank K Q + r = finrank K L by rw [← this, zero_add, Nat.add_sub_cancel]
      apply Submodule.finrank_quotient_add_finrank
    -- Hence there exists a subset of size `≥ r` in the complement of `t`,
    -- and `constantCoeff ψ` takes non-zero values on all of this subset.
    obtain ⟨s, hs⟩ := exists_finset_le_card K _ hLK
    use s \ t
    refine ⟨?_, ?_⟩
    · refine le_trans ?_ (Finset.le_card_sdiff _ _)
      omega
    · intro α hα
      simp only [Finset.mem_sdiff, Multiset.mem_toFinset, mem_roots', IsRoot.def, not_and, t] at hα
      exact hα.2 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ψ : 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
⊢ χ.coeff i = 0
have apply : ∀ i_1 ∈ s, eval i_1 (χ.coeff i) = 0
Tactic: apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ s _ ?hcard
-- 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ψ : 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
apply : ∀ i_1 ∈ s, eval i_1 (χ.coeff i) = 0
⊢ χ.coeff i = 0
have apply₁ : (χ.coeff i).natDegree < s.card
Tactic: apply eq_zero_of_natDegree_lt_card_of_eval_eq_zero' _ s _ ?hcard
-- 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ψ : 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
⊢ (χ.coeff i).natDegree < s.card
have apply : r - i < s.card
Tactic: apply lt_of_le_of_lt (lieCharpoly_coeff_natDegree _ _ _ _ i (r - i) _)
-- 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ψ : 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
apply : r - i < s.card
⊢ (χ.coeff i).natDegree < s.card
have apply₁ : i + (r - i) = finrank.{u_1, u_2} K ↥E
Tactic: apply lt_of_le_of_lt (lieCharpoly_coeff_natDegree _ _ _ _ i (r - i) _)