awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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
⊢ 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
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)
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))
⊢ Module.End.IsSemisimple (LinearMap.mulRight K a)

Tactic:
apply Module.End.isSemisimple_of_squarefree_aeval_eq_zero ha.minpoly_squarefree

Premises used: Module.End.isSemisimple_of_squarefree_aeval_eq_zero, Module.End.IsSemisimple.minpoly_squarefree
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)
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)
⊢ 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:
ext
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)
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:
simp [Algebra.lsmul]

Premises used: Algebra.lsmul
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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))

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]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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))
rw₅ rw₆ : Eq.{u_2 + 1} (α := Module.End K (Module.End K V)) 0 0
⊢ 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:
rw [hrw, Polynomial.aeval_algHom_apply, Polynomial.aeval_op_apply, minpoly.aeval,
      MulOpposite.op_zero, map_zero]

Premises used: MulOpposite.op_zero, map_zero, minpoly.aeval, Polynomial.aeval_op_apply, Polynomial.aeval_algHom_apply
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)

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]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)
hr : Module.End.IsSemisimple (LinearMap.mulRight 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

Tactic:
hl.sub_of_commute (LinearMap.commute_mulLeft_right a a) hr

Premises used: LinearMap.commute_mulLeft_right, Module.End.IsSemisimple.sub_of_commute
-- Module: Mathlib.Algebra.Lie.AdjointAction.Basic
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)
hr : Module.End.IsSemisimple (LinearMap.mulRight 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

Tactic:
exact hl.sub_of_commute (LinearMap.commute_mulLeft_right a a) hr

Premises used: LinearMap.commute_mulLeft_right, Module.End.IsSemisimple.sub_of_commute
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x y : L
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)
⊢ 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))

Tactic:
ext z
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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
H : -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆
⊢ 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:
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, LinearMap.neg_apply, coe_neg,
        Pi.neg_apply, inner_apply_apply, commutator_apply]

Premises used: LieDerivation.inner_apply_apply, LieDerivation.commutator_apply, LinearMap.neg_apply, AddHom.toFun_eq_coe, LieDerivation.coe_neg, LinearMap.coe_toAddHom, Pi.neg_apply
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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
H : -(⁅⁅z, x⁆, y⁆ + -⁅⁅z, y⁆, x⁆) = - -⁅⁅z, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆
⊢ -⁅z, ⁅x, y⁆⁆ = -⁅-⁅z, y⁆, x⁆ - -⁅-⁅z, x⁆, y⁆

Tactic:
rw [leibniz_lie, neg_lie, neg_lie, ← lie_skew x]

Premises used: leibniz_lie, neg_lie, lie_skew
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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, y⁆, x⁆ - - -⁅⁅z, x⁆, y⁆

Tactic:
abel
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
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)
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x 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:
simp
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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
⊢ (ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) = -⁅x, D⁆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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
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)
⊢ Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D =
    ⁅x, D⁆

Tactic:
ext
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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
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:
simp
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
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
⊢ Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) (LieAlgebra.center R L)

Tactic:
ext x
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
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
⊢ Membership.mem (γ := LieSubmodule R L L) (LieHom.ker (ad R L)) x ↔
    Membership.mem (γ := LieSubmodule R L L) (LieAlgebra.center R L) x

Tactic:
rw [← LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker, LieModule.mem_ker]

Premises used: LieModule.mem_ker, LieAlgebra.self_module_ker_eq_center, LieHom.mem_ker
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
x : L
⊢ 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:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
rw : Eq (α := LieIdeal R L) (LieHom.ker (ad R L)) ⊥
rw₁ : Eq (α := LieIdeal R L) (LieAlgebra.center R L) ⊥
rw₂ rw₃ : Eq.{u_2 + 1} (α := LieIdeal R L) ⊥ ⊥
⊢ Function.Injective (α := L) (β := LieDerivation R L L) (⇑(ad R L) : (a : L) → LieDerivation R L L)

Tactic:
rw [← LieHom.ker_eq_bot, ad_ker_eq_center, h]

Premises used: LieHom.ker_eq_bot, LieDerivation.ad_ker_eq_center
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
x : L
rw : ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ = -⁅x, D⁆
rw₁ :
  ⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ =
    -Bracket.bracket (L := LieDerivation R L L) ((ad R L : (a : L) → LieDerivation R L L) x : LieDerivation R L L) D
rw₂ rw₃ :
  Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
    (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
⊢ Eq (α := LieDerivation R L L) (⁅D, (ad R L : (a : L) → LieDerivation R L L) x⁆ : LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)

Tactic:
rw [ad_apply_lieDerivation, ← lie_ad, lie_skew]

Premises used: LieDerivation.ad_apply_lieDerivation, lie_skew, LieDerivation.lie_ad
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
simp_rw :
  ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
⊢ LieHom.IsIdealMorphism (L' := LieDerivation R L L) (ad R L)

Tactic:
simp_rw [LieHom.isIdealMorphism_iff, lie_der_ad_eq_ad_der]

Premises used: LieDerivation.lie_der_ad_eq_ad_der, LieHom.isIdealMorphism_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)
h :
  ∀ (x : LieDerivation R L L) (y : L),
    Eq (α := LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
w : LieDerivation R L L → L → L
⊢ ∀ (x : LieDerivation R L L) (y : L),
    ∃ (z : L),
      Eq (α := LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) ((x : (a : L) → L) y : L) : LieDerivation R L L)
        ((ad R L : (a : L) → LieDerivation R L L) z : LieDerivation R L L)

Tactic:
tauto
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
Goal:
R : Type u_1
L : Type u_2
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
D : LieDerivation R L L
⊢ Membership.mem (γ := LieIdeal R (LieDerivation R L L)) (LieHom.idealRange (ad R L)) D ↔
    ∃ (x : L), (ad R L : (a : L) → LieDerivation R L L) x = D

Tactic:
(ad R L).mem_idealRange_iff (ad_isIdealMorphism R L)

Premises used: LieDerivation.ad, LieDerivation.ad_isIdealMorphism, LieHom.mem_idealRange_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
⊢ Eq (α := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) ⊥

Tactic:
(LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Premises used: Iff.mpr, LieDerivation.ext, LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
refine :
  ∀ (D : LieDerivation R L L)
    (hD :
      Membership.mem (γ := LieSubmodule R L (LieDerivation R L L))
        (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D)
    (x : L), Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)
⊢ Eq (α := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) ⊥

Tactic:
refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_

Premises used: Iff.mpr, LieDerivation.ext, LieSubmodule.eq_bot_iff
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
rw :
  ∀ (hD : ∀ (x : L), ⁅x, D⁆ = 0) (x : L),
    Eq (α := LieDerivation R L L)
      ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L)
      (0 : LieDerivation R L L)
⊢ Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)

Tactic:
rw [LieModule.mem_maxTrivSubmodule] at hD

Premises used: LieModule.mem_maxTrivSubmodule
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
D : LieDerivation R L L
hD : ∀ (x : L), ⁅x, D⁆ = 0
x : L
⊢ Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)

Tactic:
simp [ad_apply_lieDerivation, hD]

Premises used: LieDerivation.ad_apply_lieDerivation
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
⊢ Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)

Tactic:
have : ad R L (D x) = 0 := by
    rw [LieModule.mem_maxTrivSubmodule] at hD
    simp [ad_apply_lieDerivation, hD]
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
this :
  Eq (α := LieDerivation R L L)
    ((ad R L : (a : L) → LieDerivation R L L) ((D : (a : L) → L) x : L) : LieDerivation R L L) (0 : LieDerivation R L L)
⊢ Eq (α := L) ((D : (a : L) → L) x : L) (0 : L)

Tactic:
rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this

Premises used: LieSubmodule.mem_bot, LieHom.mem_ker, LieDerivation.ad_ker_eq_center
-- Module: Mathlib.Algebra.Lie.AdjointAction.Derivation
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) ⊥
D : LieDerivation R L L
hD :
  Membership.mem (γ := LieSubmodule R L (LieDerivation R L L)) (LieModule.maxTrivSubmodule R L (LieDerivation R L L)) D
x : L
this : Eq (α := L) ((D : (a : L) → L) x : L) (0 : L)
⊢ Eq (α := L) ((D : (a : L) → L) x : L) ((0 : (a : L) → L) x : L)

Tactic:
simp [this]