awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 x_2 : K ⋊⁅ψ⁆ L
⊢ ⁅x.left, x_1.left⁆ + ⁅x.left, x_2.left⁆ +
        HAdd.hAdd (α := K) (β := K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K)
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K) -
      HAdd.hAdd (α := K) (β := K)
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K)
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K) =
    HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_1.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_1.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_1.right : LieDerivation R K K) : (a : K) → K) x.left : K) +
      HSub.hSub (β := K)
        (HAdd.hAdd (β := K) ⁅x.left, x_2.left⁆
          ((((ψ : (a : L) → LieDerivation R K K) x.right : LieDerivation R K K) : (a : K) → K) x_2.left : K))
        ((((ψ : (a : L) → LieDerivation R K K) x_2.right : LieDerivation R K K) : (a : K) → K) x.left : K)

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ ⁅x, x⁆ = 0

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst_1 : CommRing R
K : Type u_2
inst_2 : LieRing K
inst_3 : LieAlgebra R K
L : Type u_3
inst_4 : LieRing L
inst_5 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : R
x_1 x_2 : K ⋊⁅ψ⁆ L
⊢ ⁅x_1, x • x_2⁆ = x • ⁅x_1, x_2⁆

Tactic:
simp [smul_sub, smul_add]

Premises used: smul_sub, smul_add
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 : K
⊢ { left := x + x_1, right := 0 } =
    HAdd.hAdd (α := K ⋊⁅ψ⁆ L) { left := x, right := 0 : K ⋊⁅ψ⁆ L } { left := x_1, right := 0 : K ⋊⁅ψ⁆ L }

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : R
x_1 : K
⊢ { left := x • x_1, right := 0 } =
    HSMul.hSMul (α := R) (β := K ⋊⁅ψ⁆ L) ((RingHom.id R : (a : R) → R) x : R) { left := x_1, right := 0 : K ⋊⁅ψ⁆ L }

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ ∀ {x y : K},
    Eq (α := K ⋊⁅ψ⁆ L) { left := ⁅x, y⁆, right := 0 }
      (Bracket.bracket (L := K ⋊⁅ψ⁆ L) { left := x, right := 0 } { left := y, right := 0 })

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 : L
⊢ { left := 0, right := x + x_1 } =
    HAdd.hAdd (α := K ⋊⁅ψ⁆ L) { left := 0, right := x : K ⋊⁅ψ⁆ L } { left := 0, right := x_1 : K ⋊⁅ψ⁆ L }

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : R
x_1 : L
⊢ { left := 0, right := x • x_1 } =
    HSMul.hSMul (α := R) (β := K ⋊⁅ψ⁆ L) ((RingHom.id R : (a : R) → R) x : R) { left := 0, right := x_1 : K ⋊⁅ψ⁆ L }

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ ∀ {x y : L},
    Eq (α := K ⋊⁅ψ⁆ L) { left := 0, right := ⁅x, y⁆ }
      (Bracket.bracket (L := K ⋊⁅ψ⁆ L) { left := 0, right := x } { left := 0, right := y })

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K
⊢ Eq (α := K ⋊⁅ψ⁆ L) ((inl ψ : (a : K) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) ({ left := x, right := 0 } : K ⋊⁅ψ⁆ L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : L
⊢ Eq (α := K ⋊⁅ψ⁆ L) ((inr ψ : (a : L) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) ({ left := 0, right := x } : K ⋊⁅ψ⁆ L)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
a₁ : K
⊢ ∀ ⦃a₂ : K⦄,
    Eq (α := K ⋊⁅ψ⁆ L) ((inl ψ : (a : K) → K ⋊⁅ψ⁆ L) a₁ : K ⋊⁅ψ⁆ L) ((inl ψ : (a : K) → K ⋊⁅ψ⁆ L) a₂ : K ⋊⁅ψ⁆ L) →
      a₁ = a₂

Tactic:
simp [inl]

Premises used: LieAlgebra.SemiDirectSum.inl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 : K ⋊⁅ψ⁆ L
⊢ (x + x_1).right = x.right + x_1.right

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : R
x_1 : K ⋊⁅ψ⁆ L
⊢ (x • x_1).right = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) x_1.right

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ ∀ {x y : K ⋊⁅ψ⁆ L}, ⁅x, y⁆.right = ⁅x.right, y.right⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x x_1 : K ⋊⁅ψ⁆ L
⊢ (x + x_1).left = x.left + x_1.left

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : R
x_1 : K ⋊⁅ψ⁆ L
⊢ (x • x_1).left = HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R) x_1.left

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ (projr ψ : (a : K ⋊⁅ψ⁆ L) → L) x = x.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K ⋊⁅ψ⁆ L
⊢ (projl ψ : (a : K ⋊⁅ψ⁆ L) → K) x = x.left

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K
⊢ Eq.{u_3 + 1} (α := L) ((projr ψ : (a : K ⋊⁅ψ⁆ L) → L) ((inl ψ : (a : K) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) : L) (0 : L)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : L
⊢ (projr ψ : (a : K ⋊⁅ψ⁆ L) → L) ((inr ψ : (a : L) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : L
⊢ Eq.{u_2 + 1} (α := K) ((projl ψ : (a : K ⋊⁅ψ⁆ L) → K) ((inr ψ : (a : L) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) : K) (0 : K)

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K
⊢ (projl ψ : (a : K ⋊⁅ψ⁆ L) → K) ((inl ψ : (a : K) → K ⋊⁅ψ⁆ L) x : K ⋊⁅ψ⁆ L) = x

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ (inl ψ).ker = ⊥

Tactic:
simp [LieHom.ker_eq_bot]

Premises used: LieHom.ker_eq_bot
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
⊢ (projr ψ).range = ⊤

Tactic:
simp [LieHom.range_eq_top]

Premises used: LieHom.range_eq_top
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
h :
  ∀ (x : K) (y : L),
    { left := x, right := y } ∈ (inl ψ).range ↔
      { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker
⊢ (inl ψ).range = LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
ψ : LieHom.{u_1, u_3, u_2} R L (LieDerivation R K K)
x : K
y : L
⊢ { left := x, right := y } ∈ (inl ψ).range ↔
    { left := x, right := y } ∈ LieIdeal.toLieSubalgebra R (K ⋊⁅ψ⁆ L) (projr ψ).ker

Tactic:
aesop
-- Module: Mathlib.Algebra.Lie.SemiDirect
Goal:
R : Type u_1
inst : CommRing R
K : Type u_2
inst_1 : LieRing K
inst_2 : LieAlgebra R K
L : Type u_3
inst_3 : LieRing L
inst_4 : LieAlgebra R L
x x_1 : SemiDirectSum.{u_1, u_2, u_3} (R := R) K L 0
⊢ AddHom.toFun (LinearMap.toAddHom (↑(toProdl 0) : K ⋊⁅0⁆ L →ₗ[R] K × L)) ⁅x, x_1⁆ =
    ⁅AddHom.toFun (LinearMap.toAddHom (↑(toProdl 0) : K ⋊⁅0⁆ L →ₗ[R] K × L)) x,
      AddHom.toFun (LinearMap.toAddHom (↑(toProdl 0) : K ⋊⁅0⁆ L →ₗ[R] K × L)) x_1⁆

Tactic:
simp
-- Module: Mathlib.Algebra.Lie.Semisimple.Defs
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : Nontrivial M
h : ∀ (N : LieSubmodule R L M), N ≠ ⊥ → N = ⊤
⊢ IsIrreducible R L M

Tactic:
IsSimpleOrder.of_forall_eq_top h

Premises used: IsSimpleOrder.of_forall_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Defs
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieModule.IsIrreducible R L M
N : LieSubmodule R L M
inst_6 : Nontrivial.{u_3} ↥N
⊢ N = ⊤

Tactic:
(IsSimpleOrder.eq_bot_or_eq_top N).resolve_left <| (nontrivial_iff_ne_bot R L M).mp inferInstance

Premises used: inferInstance, Or.resolve_left, LieSubmodule.nontrivial_iff_ne_bot, Iff.mp, IsSimpleOrder.eq_bot_or_eq_top
-- Module: Mathlib.Algebra.Lie.Semisimple.Defs
Goal:
R : Type u_1
L : Type u_2
M : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : LieRingModule L M
inst_5 : LieAlgebra R L
inst_6 : Subsingleton L
⊢ Eq (α := LieIdeal R L) (radical R L) ⊥

Tactic:
simpa only [radical_eq_top_of_isSolvable] using Subsingleton.elim ⊤ ⊥

Premises used: LieAlgebra.radical_eq_top_of_isSolvable, Bot.bot, Subsingleton.elim, Top.top
-- 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
⊢ Nontrivial M

Tactic:
have _i := nontrivial_of_isIrreducible k L M
-- 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)), Nontrivial.{u_3} ↥(weightSpace M (⇑χ : (a : ↥(radical k L)) → k))

Tactic:
exists_nontrivial_weightSpace_of_isSolvable k (radical k L) M

Premises used: Membership.mem, Subtype, LieModule.exists_nontrivial_weightSpace_of_isSolvable, LieAlgebra.radical
-- 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
obtain :
  ∀ (χ : Dual.{u_1, u_2} k ↥(radical k L)) (hχ : Nontrivial.{u_3} ↥(weightSpace M (⇑χ : (a : ↥(radical k L)) → k))),
    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)
⊢ 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 ⟨χ, hχ⟩ : ∃ χ : Module.Dual k (radical k L), Nontrivial (weightSpace M χ) :=
    exists_nontrivial_weightSpace_of_isSolvable k (radical k L) M

Premises used: Membership.mem, Subtype, LieModule.exists_nontrivial_weightSpace_of_isSolvable, LieAlgebra.radical, Module.Dual
-- 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)
hχ : Nontrivial.{u_3} ↥(weightSpace M (⇑χ : (a : ↥(radical k L)) → k))
N : LieSubmodule k L M := weightSpaceOfIsLieTower k (A := ↥(radical k L)) M (⇑χ : (a : ↥(radical k L)) → k)
⊢ Nontrivial.{u_3} ↥N

Tactic:
replace hχ : Nontrivial N := hχ
-- 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χ : Nontrivial.{u_3} ↥N
⊢ N = ⊤

Tactic:
replace hχ : N = ⊤ := N.eq_top_of_isIrreducible k L M
-- 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χ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
h :
  ∀ (m : M),
    Eq (α := M)
      (((((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) : (a : M) → M) m : M)
      ((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 :
            (a : M) → M)
          m :
        M)
⊢ ((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

Tactic:
ext m
-- 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χ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
m : M
⊢ ∀ (y : L) (hy : Membership.mem (γ := LieIdeal k L) (radical k L) y),
    ⁅y, m⁆ =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) y hy) :
          k)
        m

Tactic:
simpa [N, weightSpaceOfIsLieTower, mem_weightSpace] using (hχ ▸ mem_top _ : m ∈ N)

Premises used: LieModule.mem_weightSpace, Eq.rec, LieModule.weightSpaceOfIsLieTower, LieSubmodule.mem_top, Eq.symm
-- 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χ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
m : M
⊢ ∀ (y : L) (hy : Membership.mem (γ := LieIdeal k L) (radical k L) y),
    ⁅y, m⁆ =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) y hy) :
          k)
        m

Tactic:
have hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m := by
      simpa [N, weightSpaceOfIsLieTower, mem_weightSpace] using (hχ ▸ mem_top _ : m ∈ N)
-- 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χ : N = ⊤
x : L
hx : Membership.mem (γ := LieIdeal k L) (radical k L) x
m : M
hm :
  ∀ (y : L) (hy : Membership.mem (γ := LieIdeal k L) (radical k L) y),
    ⁅y, m⁆ =
      HSMul.hSMul.{u_1, u_3, u_3} (α := k)
        ((χ : (a : ↥(radical k L)) → k)
            (Subtype.mk (p := fun (x : L) ↦ Membership.mem (γ := LieIdeal k L) (radical k L) x) y hy) :
          k)
        m
⊢ Eq (α := M)
    (((((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) : (a : M) → M) m : M)
    ((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 :
          (a : M) → M)
        m :
      M)

Tactic:
simpa using hm x 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χ : N = ⊤
⊢ ∀ (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

Tactic:
replace hχ (x : L) (hx : x ∈ radical k L) : toEnd k _ M x = χ ⟨x, hx⟩ • LinearMap.id := by
    ext m
    have hm : ∀ (y : L) (hy : y ∈ radical k L), ⁅y, m⁆ = χ ⟨y, hy⟩ • m := by
      simpa [N, weightSpaceOfIsLieTower, mem_weightSpace] using (hχ ▸ mem_top _ : m ∈ N)
    simpa using hm x hx