awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
suffices :
  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)
⊢ ∃ (y : End K M),
    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)
        (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)

Tactic:
suffices trace K M (φ x * y) = ∑ i, fμ i * μ i from
    ⟨y, trace_toEnd_mul_eq_zero_of_traceForm_eq_zero h y hy_range x hx, this⟩
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
⊢ Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (n * y) : K) (0 : K)

Tactic:
have htr_n : trace K M (n * y) = 0 :=
    (isNilpotent_trace_of_isNilpotent (hny_comm.isNilpotent_mul_right hn_nil)).eq_zero
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
rw :
  Eq.{u_4 + 1} (α := K) (∑ i : I, Matrix.diag ((toMatrix v v : (a : M →ₗ[K] M) → Matrix I I K) (s * y)) i)
    (∑ i : I, fμ i * μ i)
⊢ Eq.{u_4 + 1} (α := K) ((trace K M : (a : M →ₗ[K] M) → K) (s * y) : K) (∑ i : I, fμ i * μ i : K)

Tactic:
rw [trace_eq_matrix_trace _ v, Matrix.trace]

Premises used: Matrix.trace, LinearMap.trace_eq_matrix_trace
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
⊢ ∀ (x : I),
    Membership.mem (γ := Finset I) Finset.univ x →
      Matrix.diag ((toMatrix v v : (a : M →ₗ[K] M) → Matrix I I K) (s * y)) x = fμ x * μ x

Tactic:
simp [toMatrix_apply, hyv, hsv]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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) (∑ i : I, Matrix.diag ((toMatrix v v : (a : M →ₗ[K] M) → Matrix I I K) (s * y)) i)
    (∑ i : I, fμ i * μ i)

Tactic:
exact Finset.sum_congr rfl <| by simp [toMatrix_apply, hyv, hsv]

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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) (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]
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
rw₅ rw₆ : Eq.{u_4 + 1} (α := K) (∑ 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)

Tactic:
rw [hX_ns, add_mul, map_add, htr_n, htr_s, zero_add]

Premises used: add_mul, map_add, zero_add
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
⊢ FaithfulSMul R A

Tactic:
have _i : FaithfulSMul R A := FaithfulSMul.trans R (FractionRing R) A
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
⊢ Eq (α := LinearMap.BilinForm A (A ⊗[R] L)) (traceForm A (A ⊗[R] L) (A ⊗[R] M)) 0

Tactic:
simpa
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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 (↥(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
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)
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)
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries R L 1)) M

Tactic:
rw [isNilpotent_iff_forall' (R := R)]

Premises used: LieModule.isNilpotent_iff_forall'
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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 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

Premises used: LieModule.isNilpotent_iff_forall'
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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
rw : Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (LieSubmodule.baseChange A (derivedSeries R L 1)) (1 ⊗ₜ[R] x)
⊢ Membership.mem (γ := LieIdeal A (A ⊗[R] L)) (derivedSeries A (A ⊗[R] L) 1) (1 ⊗ₜ[R] x)

Tactic:
rw [derivedSeries_baseChange]

Premises used: LieAlgebra.derivedSeries_baseChange
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)) (LieSubmodule.baseChange A (derivedSeries R L 1)) (1 ⊗ₜ[R] x)

Tactic:
Submodule.tmul_mem_baseChange_of_mem 1 hx

Premises used: Set.Mem, Submodule.tmul_mem_baseChange_of_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)) (LieSubmodule.baseChange A (derivedSeries R L 1)) (1 ⊗ₜ[R] x)

Tactic:
exact Submodule.tmul_mem_baseChange_of_mem 1 hx

Premises used: Submodule.tmul_mem_baseChange_of_mem, OfNat.ofNat
-- Module: Mathlib.Algebra.Lie.CartanCriterion
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)

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