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
suffices :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal K L) (derivedSeries K L 1) x →
      _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
⊢ IsNilpotent.{u_2, u_3} (↥(derivedSeries K L 1)) M

Tactic:
suffices ∀ x ∈ derivedSeries K L 1, _root_.IsNilpotent (φ x) from
    isNilpotent_iff_forall'.mpr fun ⟨x, hx⟩ ↦ this x hx
-- 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
obtain :
  ∀ (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) (hns : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] s)
    (hn_nil : _root_.IsNilpotent n) (hs_ss : s.IsSemisimple) (hX_ns : (φ : (a : L) → End K M) x = n + s),
    _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)

Tactic:
obtain ⟨n, hn_adj, s, hns, hn_nil, hs_ss, hX_ns⟩ := (φ x).exists_isNilpotent_isSemisimple

Premises used: Module.End.exists_isNilpotent_isSemisimple
-- 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
hns : Membership.mem (γ := Subalgebra K (End K M)) K[((φ : (a : L) → End K M) x : End K M)] s
hn_nil : _root_.IsNilpotent n
hs_ss : s.IsSemisimple
hX_ns : (φ : (a : L) → End K M) x = n + s
⊢ Commute n s

Tactic:
replace hns : Commute n s :=
    commute_of_mem_adjoin_singleton_of_commute hns (commute_of_mem_adjoin_self hn_adj).symm
-- 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
this : s = 0
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)

Tactic:
aesop
-- 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
suffices : s = 0
⊢ _root_.IsNilpotent.{u_3} (R := End K M) ((φ : (a : L) → End K M) x : End K M)

Tactic:
suffices s = 0 by aesop
-- 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 μ)
have : ∀ (this : Fintype I), s = 0
⊢ s = 0

Tactic:
have : Fintype I := FiniteDimensional.fintypeBasisIndex v
-- 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 ν)))
⊢ ∀ (i : I), (s : (a : M) → M) ((v : (a : I) → M) i : M) = HSMul.hSMul (β := M) (μ i) ((v : (a : I) → M) i : M)

Tactic:
have hsv (i : I) : s (v i) = μ i • v i :=
    mem_eigenspace_iff.mp (eigenDecomp.collectedBasis_mem _ i)
-- 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 μ)
⊢ ∀ (i : I), μ i ∈ E

Tactic:
have hμ (i : I) : μ i ∈ E := Submodule.subset_span (Set.mem_range_self i)
-- 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_1 : 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
this : ∀ (f : Dual ℚ ↥E), f = 0
suffices : ∀ (ν : K), s.HasEigenvalue ν → ν = 0
⊢ s = 0

Tactic:
suffices ∀ ν, s.HasEigenvalue ν → ν = 0 from hs_ss.eq_zero_iff_forall_eigenvalue.mpr 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_1 : 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
this : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
hν : s.HasEigenvalue ν
⊢ Nontrivial.{u_3} ↥(s.eigenspace ν)

Tactic:
have : Nontrivial (s.eigenspace ν) :=
      Submodule.nontrivial_iff_ne_bot.mpr (hasEigenvalue_iff.mp hν)
-- 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_1 : 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
this_2 : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
hν : s.HasEigenvalue ν
this : Nontrivial.{u_3} ↥(s.eigenspace ν)
⊢ ν ∈ E

Tactic:
replace hν : ν ∈ E := Submodule.subset_span ⟨⟨ν, ⟨0, finrank_pos⟩⟩, 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_1 : 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
this_2 : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
this : Nontrivial.{u_3} ↥(s.eigenspace ν)
hν : ν ∈ E
⊢ ∀ (a b : Dual ℚ ↥E), a = b

Tactic:
aesop
-- 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_1 : 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
this_2 : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
this : Nontrivial.{u_3} ↥(s.eigenspace ν)
hν : ν ∈ E
⊢ Subsingleton.{u_4 + 1} ↥E

Tactic:
have : Subsingleton E := (subsingleton_dual_iff ℚ).mp ⟨by aesop⟩
-- 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_1 : 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
this_2 : ∀ (f : Dual ℚ ↥E), f = 0
ν : K
this_3 : Nontrivial.{u_3} ↥(s.eigenspace ν)
hν : ν ∈ E
this : Subsingleton.{u_4 + 1} ↥E
⊢ ν = 0

Tactic:
simpa using Subsingleton.elim (⟨ν, hν⟩ : E) 0

Premises used: Subtype.mk, Subsingleton.elim, OfNat.ofNat
-- 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
suffices : ∀ (f : Dual ℚ ↥E), f = 0
⊢ s = 0

Tactic:
suffices ∀ f : Dual ℚ E, f = 0 by
    suffices ∀ ν, s.HasEigenvalue ν → ν = 0 from hs_ss.eq_zero_iff_forall_eigenvalue.mpr this
    intro ν hν
    have : Nontrivial (s.eigenspace ν) :=
      Submodule.nontrivial_iff_ne_bot.mpr (hasEigenvalue_iff.mp hν)
    replace hν : ν ∈ E := Submodule.subset_span ⟨⟨ν, ⟨0, finrank_pos⟩⟩, rfl⟩
    have : Subsingleton E := (subsingleton_dual_iff ℚ).mp ⟨by aesop⟩
    simpa using Subsingleton.elim (⟨ν, hν⟩ : E) 0
-- 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_1 : 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
this : ∀ (i : I), Eq (α := ℚ) ((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯) : ℚ) (0 : ℚ)
rw :
  ∀ (s : (↑(Set.range μ) : Type u_4)),
    Eq (α := ℚ) ((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑s : K) ⋯) : ℚ) (0 : ℚ)
⊢ f = 0

Tactic:
rw [Submodule.linearMap_eq_zero_iff_of_eq_span f rfl]

Premises used: Submodule.linearMap_eq_zero_iff_of_eq_span, 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_1 : 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
this : ∀ (i : I), Eq (α := ℚ) ((f : (a : ↥E) → ℚ) (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (μ i) ⋯) : ℚ) (0 : ℚ)
i : I
⊢ Eq (α := ℚ)
    ((f : (a : ↥E) → ℚ)
        (Subtype.mk (p := fun (x : K) ↦ x ∈ E) (↑(Subtype.mk (p := fun (x : K) ↦ x ∈ Set.range μ) (μ i) ⋯) : K) ⋯) :
      ℚ)
    (0 : ℚ)

Tactic:
this i