awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
Tactic: have htr_s : trace K M (s * y) = ∑ i, fμ i * μ i := by
    rw [trace_eq_matrix_trace _ v, Matrix.trace]
    exact Finset.sum_congr rfl <| by simp [toMatrix_apply, hyv, hsv]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw₁ : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y + s * y) : K) (∑ i : I, fμ i * μ i : K)
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
rw₁ : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y + s * y) : K) (∑ i : I, fμ i * μ i : K)
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw₂ : HAdd.hAdd (α := K) (β := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K)
    ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) =
  ∑ i : I, fμ i * μ i
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
rw₁ : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y + s * y) : K) (∑ i : I, fμ i * μ i : K)
rw₂ :
  HAdd.hAdd (α := K) (β := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K)
      ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) =
    ∑ i : I, fμ i * μ i
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw₃ : HAdd.hAdd (α := K) (β := K) (0 : K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) = ∑ i : I, fμ i * μ i
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
rw₁ : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y + s * y) : K) (∑ i : I, fμ i * μ i : K)
rw₂ :
  HAdd.hAdd (α := K) (β := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K)
      ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) =
    ∑ i : I, fμ i * μ i
rw₃ : HAdd.hAdd (α := K) (β := K) (0 : K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) = ∑ i : I, fμ i * μ i
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw₄ : HAdd.hAdd (α := K) 0 (∑ i : I, fμ i * μ i) = ∑ i : I, fμ i * μ i
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
L : Type u_2
M : Type u_3
inst : LieRing L
inst_1 : AddCommGroup M
inst_2 : LieRingModule L M
K : Type u_4
inst_3 : Field K
inst_4 : CharZero K
inst_5 : IsAlgClosed K
inst_6 : LieAlgebra K L
inst_7 : Module K M
inst_8 : LieModule K L M
inst_9 : FiniteDimensional K M
h : Eq (α := LinearMap.BilinForm K L) (traceForm K L M) 0
φ : LieHom.{u_4, u_2, u_3} K L (End K M) := toEnd K L M
x : L
hx : Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x
n : End K M
hn_adj : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] n
s : End K M
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
hns : Commute n s
eigenDecomp : DirectSum.IsInternal s.eigenspace := ⋯
I : Type (max u_4 0) := (ν : K) × Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))
v : Basis I K M :=
  eigenDecomp.collectedBasis (α := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν))) fun (μ : K) ↦
    finBasis K ↥(s.eigenspace μ)
this : Fintype I
μ : I → K := Sigma.fst (β := fun (ν : K) ↦ Fin (finrank.{u_4, u_3} K ↥(s.eigenspace ν)))
hsv : ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)
E : Submodule ℚ K := Submodule.span ℚ (Set.range μ)
hμ : ∀ (i : I), μ i ∈ E
f : Dual ℚ ↥E
fμ : (i : I) → K := fun (i : I) ↦ (↑((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯)) : K)
y : End K M := (Matrix.toLin v v : (a : Matrix I I K) → M →ₗ[K] M) (Matrix.diagonal fμ)
hyv : ∀ (i : I), (y : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (fμ i) ((v : (a : I) → M) i : M)
hy_range : ∀ (z : End K M) (hz : z ∈ φ.range), ⁅y, z⁆ ∈ φ.range
hny_comm : Commute n y
htr_n : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)
htr_s : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)
rw : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) ((n + s) * y) : K) (∑ i : I, fμ i * μ i : K)
rw₁ : Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y + s * y) : K) (∑ i : I, fμ i * μ i : K)
rw₂ :
  HAdd.hAdd (α := K) (β := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K)
      ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) =
    ∑ i : I, fμ i * μ i
rw₃ : HAdd.hAdd (α := K) (β := K) (0 : K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) = ∑ i : I, fμ i * μ i
rw₄ : HAdd.hAdd (α := K) 0 (∑ i : I, fμ i * μ i) = ∑ i : I, fμ i * μ i
⊢ Eq.{u_4 + 1} (α := K)
    ((trace K M : (a : M →ₗ[K] M) → K) (HMul.hMul (α := End K M) ((φ : (a : L) → End K M) x : End K M) y) : K)
    (∑ i : I, fμ i * μ i : K)
have rw₅ : Eq.{u_4 + 1} (α := K) (∑ i : I, fμ i * μ i) (∑ i : I, fμ i * μ i)
Tactic: rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries R L 1)) M
have _i : FaithfulSMul R A
Tactic: have _i : FaithfulSMul R A := FaithfulSMul.trans R (FractionRing R) A
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries R L 1)) M
have nilp_ext : IsNilpotent (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)
Tactic: have nilp_ext : IsNilpotent (derivedSeries A (A ⊗[R] L) 1) (A ⊗[R] M) :=
    isNilpotent_derivedSeries_of_traceForm_eq_zero_aux <| by simpa
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext : IsNilpotent (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries R L 1)) M
have rw : ∀ (x : ↥(derivedSeries R L 1)),
  _root_.IsNilpotent.{u_3} (R := End R M)
    ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M) x : End R M)
Tactic: rw [isNilpotent_iff_forall' (R := R)]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext : IsNilpotent (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M)
⊢ ∀ (x : ↥(derivedSeries R L 1)),
    _root_.IsNilpotent.{u_3} (R := End R M)
      ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M) x : End R M)
have nilp_ext₁ : ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
  _root_.IsNilpotent (R := End A (A ⊗[R] M))
    ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
        x :
      End A (A ⊗[R] M))
Tactic: rw [isNilpotent_iff_forall' (R := A)] at nilp_ext
Cleared hypotheses: nilp_ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (goal)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
    _root_.IsNilpotent (R := End A (A ⊗[R] M))
      ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
          x :
        End A (A ⊗[R] M))
x : L
hx : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
⊢ Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)
have rw : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L 1)) (1 ⊗ₜ[R] x)
Tactic: rw [derivedSeries_baseChange]
-- Lean 4 proof step from Mathlib.Algebra.Lie.CartanCriterion (hypothesis)
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : CharZero R
inst_2 : IsDomain R
inst_3 : LieRing L
inst_4 : LieAlgebra R L
inst_5 : AddCommGroup M
inst_6 : LieRingModule L M
inst_7 : Module R M
inst_8 : LieModule R L M
inst_9 : IsNoetherian R M
inst_10 : Free R M
h : Eq (α := LinearMap.BilinForm R L) (traceForm R L M) 0
A : Type u_1 := AlgebraicClosure (FractionRing R)
_i : FaithfulSMul R A
nilp_ext :
  ∀ (x : ↥(derivedSeries A (A ⊗[R] L) 1)),
    _root_.IsNilpotent (R := End A (A ⊗[R] M))
      ((toEnd A (↥(derivedSeries A (A ⊗[R] L) 1)) (A ⊗[R] M) : (a : ↥(derivedSeries A (A ⊗[R] L) 1)) → End A (A ⊗[R] M))
          x :
        End A (A ⊗[R] M))
x : L
hx : Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x
⊢ _root_.IsNilpotent.{u_3} (R := End R M)
    ((toEnd R (↥(derivedSeries R L 1)) M : (a : ↥(derivedSeries R L 1)) → End R M)
        (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal R L) (derivedSeries R L 1) x) x hx) :
      End R M)
have hx_ext : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)
Tactic: have hx_ext : 1 ⊗ₜ[R] x ∈ derivedSeries A (A ⊗[R] L) 1 := by
    rw [derivedSeries_baseChange]
    exact Submodule.tmul_mem_baseChange_of_mem 1 hx