Algebra · medium

Statement, exactly as the model and Lean see it

theorem lg_target (K : Type u_7) {L : Type u_8} [Field K] [LieRing L] [LieAlgebra K L] [Module.Finite K L] (x : L) : Module.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((LieAlgebra.ad K L) x)).natTrailingDegree := by

Mathlib declaration: LieAlgebra.finrank_engel
Held-out module: Mathlib.Algebra.Lie.Rank
Banned modules (itself + downstream): 2
Reference proof premises (reachable / held-out): 3 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00013

Attempts

sample 0 · round 0Wrong tactic4.6 s model time

Proof

intro x
let S := LieSubalgebra.engel K x
have hS : LieSubalgebra K S := by apply LieSubalgebra.isLieSubalgebra
have hK : IsLieAlgebra K S := by apply IsLieAlgebra.ofIsLieRingAndModule
have hM : Module K S := by apply Module.ofIsModule
have hF : FiniteDimensional K S := by apply Module.Finite.ofModuleFinite
have hFD : FiniteDimensional K S := hF
let f := LinearMap.charpoly (LieAlgebra.ad K L x)
let p := f.natTrailingDegree
have hP : p = Module.finrank K S := by
  apply eq_of_le_of_ge
  rw [Module.finrank_le_dim]
  apply Nat.le_refl
  rw [Module.dim_le_finrank]
  apply Nat.le_refl
  exact Module.finrank_eq_dim
exact hP

What Lean printed (this is all the model sees on repair)

4:8: error: Tactic `introN` failed: There are no additional binders or `let` bindings in the goal to introduce

K : Type u_7
L : Type u_8
inst✝³ : Field K
inst✝² : LieRing L
inst✝¹ : LieAlgebra K L
inst✝ : Module.Finite K L
x : L
⊢ Module.finrank K ↥(LieSubalgebra.engel K x) = (LinearMap.charpoly ((LieAlgebra.ad K L) x)).natTrailingDegree

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

lemma finrank_engel (x : L) :
    finrank K (engel K x) = (ad K L x).charpoly.natTrailingDegree :=
  (ad K L x).finrank_maxGenEigenspace_zero_eq