awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
⊢ Eq (α := LieIdeal k L) (radical k L) (center k L)

Tactic:
le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)

Premises used: Iff.mpr, LieModule.mem_maxTrivSubmodule, LieAlgebra.center_le_radical, le_antisymm
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
refine : ∀ (x : L) (hx : Membership.mem (γ := LieSubmodule k L L) (radical k L) x) (x_1 : L), ⁅x_1, x⁆ = 0
⊢ Eq (α := LieIdeal k L) (radical k L) (center k L)

Tactic:
refine le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)

Premises used: LieAlgebra.center_le_radical, le_antisymm
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (radical k L) x
y : L
⊢ ⁅y, x⁆ = 0

Tactic:
simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), LieHom.map_lie, hχ _ hx, lie_smul,
      (toEnd k L M y).commute_id_right.lie_eq]

Premises used: Commute.lie_eq, lie_smul, LieHom.map_lie, Module.End.commute_id_right, LieModule.toEnd_eq_zero_iff, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
⊢ Eq (α := LieIdeal k L) (radical k L) (center k L)

Tactic:
have aux : radical k L = center k L := by
    refine le_antisymm (fun x hx ↦ (mem_maxTrivSubmodule k L L x).mpr ?_) (center_le_radical k L)
    intro y
    simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), LieHom.map_lie, hχ _ hx, lie_smul,
      (toEnd k L M y).commute_id_right.lie_eq]
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
⟨⟨aux⟩, fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ (mem_maxTrivSubmodule k L L x).mpr fun y ↦ ?_⟩⟩

Premises used: Iff.mpr, LieAlgebra.HasCentralRadical.mk, LieModule.mem_maxTrivSubmodule, And.intro, Iff.intro
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
refine_1 :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (center k L) x),
    Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
      (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
refine_2 :
  ∀ (x : L)
    (hx :
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M))
    (y : L), ⁅y, x⁆ = 0
⊢ HasCentralRadical k L ∧
    ∀ (x : L),
      Membership.mem (γ := LieIdeal k L) (center k L) x ↔
        Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
refine ⟨⟨aux⟩, fun x ↦ ⟨fun hx ↦ ?_, fun hx ↦ (mem_maxTrivSubmodule k L L x).mpr fun y ↦ ?_⟩⟩
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx : Membership.mem (γ := LieIdeal k L) (center k L) x
⊢ Membership.mem (γ := LieIdeal k L) (radical k L) x

Tactic:
rw [← aux] at hx
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
⊢ Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
Submodule.mem_span_singleton.mpr ⟨χ ⟨x, hx⟩, (hχ x hx).symm⟩

Premises used: Iff.mpr, Set.Mem, setOf, Submodule.mem_span_singleton, Subtype.mk, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
⊢ Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
exact Submodule.mem_span_singleton.mpr ⟨χ ⟨x, hx⟩, (hχ x hx).symm⟩

Premises used: Iff.mpr, Submodule.mem_span_singleton, Subtype.mk, Exists.intro, Eq.symm, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
y : L
refine_2 :
  ∀ (t : k)
    (ht :
      HSMul.hSMul (β := End k M) t LinearMap.id =
        ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x),
    ⁅y, x⁆ = 0
⊢ ⁅y, x⁆ = 0

Tactic:
obtain ⟨t, ht⟩ := Submodule.mem_span_singleton.mp hx

Premises used: Submodule.mem_span_singleton, Iff.mp
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
_i : Nontrivial M
χ : Dual.{u_1, u_2} k ↥(radical k L)
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
hχ :
  ∀ (x : L) (hx : Membership.mem (γ := LieIdeal k L) (radical k L) x),
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k) (β := M →ₗ[k] M)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) x hx) :
          k)
        LinearMap.id
aux : Eq (α := LieIdeal k L) (radical k L) (center k L)
x : L
hx :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
y : L
t : k
ht :
  HSMul.hSMul (β := End k M) t LinearMap.id =
    ((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x
⊢ ⁅y, x⁆ = 0

Tactic:
simp [← toEnd_eq_zero_iff (R := k) (L := L) (M := M), LieHom.map_lie, ← ht, lie_smul,
      (toEnd k L M y).commute_id_right.lie_eq]

Premises used: Commute.lie_eq, lie_smul, LieHom.map_lie, Module.End.commute_id_right, LieModule.toEnd_eq_zero_iff, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
⊢ finrank k M ≠ 0

Tactic:
have : finrank k M ≠ 0 := (finrank_pos_iff.mpr <| nontrivial_of_isIrreducible k L M).ne'
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
⊢ HasCentralRadical k L

Tactic:
obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M

Premises used: LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
⊢ ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
obtain ⟨_i, h'⟩ := hasCentralRadical_and_of_isIrreducible_of_isFaithful k L M

Premises used: LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
rw : ∀ (m : L), Membership.mem (γ := LieSubmodule k L L) (center k L) m → m = 0
⊢ HasTrivialRadical k L

Tactic:
rw [hasTrivialRadical_iff, (hasCentralRadical_iff k L).mp inferInstance, LieSubmodule.eq_bot_iff]

Premises used: LieAlgebra.hasCentralRadical_iff, LieAlgebra.hasTrivialRadical_iff, inferInstance, Iff.mp, LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
h :
  ∀ (x : L),
    Eq.{u_1 + 1} (α := k)
      ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
          (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
        k)
      (0 : k)
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (center k L) x
⊢ Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)

Tactic:
specialize h x
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (center k L) x
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
⊢ Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)

Tactic:
rw [h' x] at hx
-- Module: Mathlib.Algebra.Lie.Semisimple.Lemmas
Goal:
k : Type u_1
L : Type u_2
M : Type u_3
inst : Field k
inst_1 : CharZero k
inst_2 : LieRing L
inst_3 : LieAlgebra k L
inst_4 : Module.Finite k L
inst_5 : AddCommGroup M
inst_6 : Module k M
inst_7 : LieRingModule L M
inst_8 : LieModule k L M
inst_9 : Module.Finite k M
inst_10 : IsIrreducible k L M
inst_11 : IsFaithful k L M
inst_12 : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' :
  ∀ (x : L),
    Membership.mem (γ := LieIdeal k L) (center k L) x ↔
      Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
x : L
hx : Membership.mem (γ := LieSubmodule k L L) (center k L) x
h :
  Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)
hx₁ :
  Membership.mem (α := End k M) (γ := Submodule k (M →ₗ[k] M)) (k ∙ LinearMap.id)
    (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M)
⊢ Eq.{u_1 + 1} (α := k)
    ((LinearMap.trace k M : (a : M →ₗ[k] M) → k)
        (((toEnd k L M : LieHom.{u_1, u_2, u_3} k L (End k M)) : (a : L) → End k M) x : End k M) :
      k)
    (0 : k)

Tactic:
rw [h' x] at hx