awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V))
        ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a) : Module.End K V) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) 0 :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₂ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V)) 0 0
Tactic: rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulLeft K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have this : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  (((Polynomial.aeval ((Algebra.lmul K (Module.End K V) : (a : Module.End K V) → Module.End K (Module.End K V)) a) :
          AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
        (a : Polynomial K) → Module.End K (Module.End K V))
      (minpoly K a) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: have : Polynomial.aeval (Algebra.lmul K (Module.End K V) a) (minpoly K a) = 0 := by
      rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
⊢ (HSub.hSub (α := (a : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (β :=
      (b : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulLeft K) (LinearMap.mulRight K)
      a).IsSemisimple
have hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
Tactic: have hl : Module.End.IsSemisimple (LinearMap.mulLeft K a) := by
    apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
    have : Polynomial.aeval (Algebra.lmul K (Module.End K V) a) (minpoly K a) = 0 := by
      rw [Polynomial.aeval_algHom_apply, minpoly.aeval, map_zero]
    simpa using this
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ Module.End.IsSemisimple (LinearMap.mulRight K a)
have apply : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
have h : ∀ (x : Module.End K V) (x_1 : V),
  Eq (α := V)
    ((((LinearMap.mulRight K a : (a : Module.End K V) → Module.End K V) x : Module.End K V) : (a : V) → V) x_1 : V)
    ((((((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                    (MulOpposite.op a) :
                  Module.End K (Module.End K V)) :
                (a : Module.End K V) → Module.End K V)
              x :
            Module.End K V) :
          (a : V) → V)
        x_1 :
      V)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have hrw : Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
  ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V)) (MulOpposite.op a))
Tactic: have hrw : LinearMap.mulRight K a =
        (Algebra.lsmul (A := (Module.End K V)ᵐᵒᵖ) K K (Module.End K V)) (.op a) := by
      ext; simp [Algebra.lsmul]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  (((Polynomial.aeval
            ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
              (MulOpposite.op a)) :
          AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
        (a : Polynomial K) → Module.End K (Module.End K V))
      (minpoly K a) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval
              ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                (MulOpposite.op a)) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₁ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      ((Polynomial.aeval (MulOpposite.op a) : (a : Polynomial K) → (Module.End K V)ᵐᵒᵖ) (minpoly K a) :
        (Module.End K V)ᵐᵒᵖ) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval
              ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                (MulOpposite.op a)) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        ((Polynomial.aeval (MulOpposite.op a) : (a : Polynomial K) → (Module.End K V)ᵐᵒᵖ) (minpoly K a) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₂ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a)) :
        (Module.End K V)ᵐᵒᵖ) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval
              ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                (MulOpposite.op a)) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        ((Polynomial.aeval (MulOpposite.op a) : (a : Polynomial K) → (Module.End K V)ᵐᵒᵖ) (minpoly K a) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₂ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        (MulOpposite.op ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a)) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₃ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V)) (MulOpposite.op 0) :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval
              ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                (MulOpposite.op a)) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        ((Polynomial.aeval (MulOpposite.op a) : (a : Polynomial K) → (Module.End K V)ᵐᵒᵖ) (minpoly K a) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₂ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        (MulOpposite.op ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a)) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₃ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        (MulOpposite.op 0) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₄ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
  ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V)) 0 :
    Module.End K (Module.End K V))
  (0 : Module.End K (Module.End K V))
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (goal)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
hrw :
  Eq (α := Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulRight K a)
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
      (MulOpposite.op a))
rw :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    (((Polynomial.aeval
              ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
                (MulOpposite.op a)) :
            AlgHom.{u_1, u_1, u_2} K (Polynomial K) (Module.End K (Module.End K V))) :
          (a : Polynomial K) → Module.End K (Module.End K V))
        (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₁ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        ((Polynomial.aeval (MulOpposite.op a) : (a : Polynomial K) → (Module.End K V)ᵐᵒᵖ) (minpoly K a) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₂ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        (MulOpposite.op ((Polynomial.aeval a : (a : Polynomial K) → Module.End K V) (minpoly K a)) :
          (Module.End K V)ᵐᵒᵖ) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₃ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V))
        (MulOpposite.op 0) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
rw₄ :
  Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Algebra.lsmul K K (Module.End K V) : (a : (Module.End K V)ᵐᵒᵖ) → Module.End K (Module.End K V)) 0 :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
⊢ Eq.{u_2 + 1} (α := Module.End K (Module.End K V))
    ((Polynomial.aeval (LinearMap.mulRight K a) : (a : Polynomial K) → Module.End K (Module.End K V)) (minpoly K a) :
      Module.End K (Module.End K V))
    (0 : Module.End K (Module.End K V))
have rw₅ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V)) 0 0
Tactic: rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Basic (hypothesis)
Goal:
K : Type u_1
V : Type u_2
inst : Field K
inst_1 : PerfectField K
inst_2 : AddCommGroup V
inst_3 : Module K V
inst_4 : FiniteDimensional K V
a : Module.End K V
ha : a.IsSemisimple
hl : Module.End.IsSemisimple (LinearMap.mulLeft K a)
⊢ (HSub.hSub (α := (a : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (β :=
      (b : Module.End K V) → Module.End K V →ₗ[K] Module.End K V) (LinearMap.mulLeft K) (LinearMap.mulRight K)
      a).IsSemisimple
have hr : Module.End.IsSemisimple (LinearMap.mulRight K a)
Tactic: have hr : Module.End.IsSemisimple (LinearMap.mulRight K a) := by
    apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree
    have hrw : LinearMap.mulRight K a =
        (Algebra.lsmul (A := (Module.End K V)ᵐᵒᵖ) K K (Module.End K V)) (.op a) := by
      ext; simp [Algebra.lsmul]
    rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
⊢ Eq (α := LieDerivation R L L) (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) ⁅x, y⁆)
    (Bracket.bracket (L := LieDerivation R L L) (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) x)
      (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) y))
have H : ∀ (z : L),
  Eq (α := L) ((AddHom.toFun (LinearMap.toAddHom (-inner R L L)) ⁅x, y⁆ : (a : L) → L) z : L)
    ((Bracket.bracket (L := LieDerivation R L L) (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) x)
            (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) y) :
          (a : L) → L)
        z :
      L)
Tactic: ext z
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y z : L
⊢ Eq (α := L) ((AddHom.toFun (LinearMap.toAddHom (-inner R L L)) ⁅x, y⁆ : (a : L) → L) z : L)
    ((Bracket.bracket (L := LieDerivation R L L) (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) x)
            (AddHom.toFun (LinearMap.toAddHom (-inner R L L)) y) :
          (a : L) → L)
        z :
      L)
have H : -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
Tactic: simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.neg_apply, coe_neg,
        Pi.neg_apply, inner_apply_apply, commutator_apply]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y z : L
⊢ -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
have H : -(⁅⁅z, x⁆, y⁆ + -⁅⁅z, y⁆, x⁆) = - -⁅⁅z, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆
Tactic: rw [leibniz_lie, neg_lie, neg_lie, ← lie_skew x]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ Eq.{u_2 + 1} (α := L →ₗ[R] L) (↑((ad R L : (a : L) → LieDerivation R L L) x) : L →ₗ[R] L)
    ((LieAlgebra.ad R L : (a : L) → Module.End R L) x)
have h : ∀ (x_1 : L),
  Eq (α := L) (((↑((ad R L : (a : L) → LieDerivation R L L) x) : L →ₗ[R] L) : (a : L) → L) x_1 : L)
    ((((LieAlgebra.ad R L : (a : L) → Module.End R L) x : Module.End R L) : (a : L) → L) x_1 : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
D : LieDerivation R L L
⊢ Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D =
    ⁅x, D⁆
have H : ∀ (a : L),
  Eq (α := L)
    ((Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D :
          (a : L) → L)
        a :
      L)
    ((⁅x, D⁆ : (a : L) → L) a : L)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (LieAlgebra.center R L)
have h : ∀ (x : L),
  Membership.mem (γ := LieSubmodule R L L) (LieHom.ker (ad R L)) x ↔
    Membership.mem (γ := LieSubmodule R L L) (LieAlgebra.center R L) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ Membership.mem (γ := LieSubmodule R L L) (LieHom.ker (ad R L)) x ↔
    Membership.mem (γ := LieSubmodule R L L) (LieAlgebra.center R L) x
have h : Eq (α := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L)
    (0 : LieDerivation R L L) ↔
  ∀ (m : L), ⁅x, m⁆ = 0
Tactic: rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Lie.AdjointAction.Derivation (goal)
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
h : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
⊢ Function.Injective (α := L) (β := LieDerivation R L L) (⇑(ad R L) : (a : L) → LieDerivation R L L)
have rw : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) ⊥
Tactic: rw [← LieHom.ker_eq_bot, ad_ker_eq_center, h]