-- Mathlib/Algebra/Lie/Semisimple/Lemmas.lean
theorem hasTrivialRadical_and_of_isIrreducible_of_isFaithful
    (h : ∀ x, LinearMap.trace k _ (toEnd k L M x) = 0) : HasTrivialRadical k L

Proof state:
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
this : finrank k M ≠ 0
⊢ HasTrivialRadical k L

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

Result:
case intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
⊢ HasTrivialRadical k L

Proof state:
case intro.intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
x : L
hx : (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
t : k
ht : t • LinearMap.id = (toEnd k L M) x
⊢ t = 0

Tactic:
simpa [this, ← ht] using h

Result:
no goals

Proof state:
case intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
h : ∀ (x : L), (LinearMap.trace k M) ((toEnd k L M) x) = 0
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
x : L
hx : x ∈ center k L
⊢ x = 0

Tactic:
specialize h x

Result:
case intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
x : L
hx : x ∈ center k L
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
⊢ x = 0

Proof state:
case intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
x : L
hx : x ∈ center k L
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
⊢ x = 0

Tactic:
rw [h' x] at hx

Result:
case intro
k : Type u_1
L : Type u_2
M : Type u_3
inst✝¹² : Field k
inst✝¹¹ : CharZero k
inst✝¹⁰ : LieRing L
inst✝⁹ : LieAlgebra k L
inst✝⁸ : Module.Finite k L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module k M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule k L M
inst✝³ : Module.Finite k M
inst✝² : LieModule.IsIrreducible k L M
inst✝¹ : IsFaithful k L M
inst✝ : IsTriangularizable k L M
this : finrank k M ≠ 0
_i : HasCentralRadical k L
h' : ∀ (x : L), x ∈ center k L ↔ (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
x : L
hx : (toEnd k L M) x ∈ Submodule.span k {LinearMap.id}
h : (LinearMap.trace k M) ((toEnd k L M) x) = 0
⊢ x = 0