awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M) =
    m
e_s :
  ∃ (x_1 : ↥I) (n_1 : ↥N),
    ⁅(↑x_1 : L), (↑n_1 : M)⁆ =
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
        (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
            ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
          L ⊗[R] M)
⊢ ∃ (x : ↥I) (n : ↥N), ⁅(↑x : L), (↑n : M)⁆ = m

Tactic:
rw [← h]
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M) =
    m
h₁ :
  ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆ =
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M)
⊢ ∃ (x_1 : ↥I) (n_1 : ↥N),
    ⁅(↑x_1 : L), (↑n_1 : M)⁆ =
      ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
        (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
            ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
          L ⊗[R] M)

Tactic:
use ⟨x, hx⟩, ⟨n, hn⟩
-- Module: Mathlib.Algebra.Lie.TensorProduct
Goal:
R : Type u
inst : CommRing R
L : Type v
M : Type w
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
I : LieIdeal R L
N : LieSubmodule R L M
m : M
x : L
hx : x ∈ I
n : M
hn : n ∈ N
h :
  ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M) =
    m
⊢ ⁅(↑(Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) : L), (↑(Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) : M)⁆ =
    ((↑(toModuleHom R L M) : L ⊗[R] M →ₗ[R] M) : (a : L ⊗[R] M) → M)
      (((↑(incl I) : ↥I →ₗ[R] L) : (a : ↥I) → L) (Subtype.mk (p := fun (x : L) ↦ x ∈ I) x hx) ⊗ₜ[R]
          ((↑N.incl : ↥N →ₗ[R] M) : (a : ↥N) → M) (Subtype.mk (p := fun (x : M) ↦ x ∈ N) n hn) :
        L ⊗[R] M)

Tactic:
rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y) :
      R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) y : R)
    ((((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) x : R)

Tactic:
LinearMap.trace_mul_comm R (φ x) (φ y)

Premises used: LinearMap.trace_mul_comm, LieModule.toEnd, DFunLike.coe
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ LinearMap.IsSymm (traceForm R L M)

Tactic:
⟨LieModule.traceForm_comm R L M⟩

Premises used: LieModule.traceForm_comm, LinearMap.IsSymm.mk
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
⊢ Eq (α := L →ₗ[R] L →ₗ[R] R) (LinearMap.flip (traceForm R L M)) (traceForm R L M)

Tactic:
Eq.symm <| LinearMap.ext₂ <| traceForm_comm R L M

Premises used: LieModule.traceForm_comm, LinearMap.ext₂, Eq.symm
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
      R)

Tactic:
simp only [traceForm_apply_apply]

Premises used: LieModule.traceForm_apply_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (β := End R M)
          (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
            HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) :
      R)

Tactic:
?_
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ (trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (β := End R M)
        (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
          HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)

Tactic:
?_
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
        R)

Tactic:
?_
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
        R) =
    (((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆

Tactic:
?_
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ Eq.{u_1 + 1} (α := R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) ⁅x, y⁆ ∘ₗ
          ((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z) :
      R)
    ((trace R M : (a : M →ₗ[R] M) → R)
        (HMul.hMul (β := End R M)
          (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
            HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
          (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) :
      R)

Tactic:
simp only [LieHom.map_lie, Ring.lie_def, ← Module.End.mul_eq_comp]

Premises used: Module.End.mul_eq_comp, LieHom.map_lie, Ring.lie_def
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ (trace R M : (a : M →ₗ[R] M) → R)
      (HMul.hMul (β := End R M)
        (HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M) -
          HMul.hMul (α := End R M) (β := End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M))
        (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)

Tactic:
simp only [sub_mul, map_sub, mul_assoc]

Premises used: map_sub, mul_assoc, sub_mul
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R) =
    HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
        R)

Tactic:
simp only [LinearMap.trace_mul_cycle' R (φ x) (φ z) (φ y)]
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
⊢ HSub.hSub (α := R) (β := R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M))) :
        R)
      ((trace R M : (a : M →ₗ[R] M) → R)
          (HMul.hMul (α := End R M) (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) x : End R M)
            (HMul.hMul (α := End R M) (β := End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) z : End R M)
              (((φ : LieHom.{u_1, u_3, u_4} R L (End R M)) : (a : L) → End R M) y : End R M))) :
        R) =
    (((traceForm R L M : (a : L) → L →ₗ[R] R) x : L →ₗ[R] R) : (a : L) → R) ⁅y, z⁆

Tactic:
simp only [traceForm_apply_apply, LieHom.map_lie, Ring.lie_def, mul_sub, map_sub,
      ← Module.End.mul_eq_comp]

Premises used: map_sub, Module.End.mul_eq_comp, mul_sub, LieHom.map_lie, LieModule.traceForm_apply_apply, Ring.lie_def
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
rw₂ rw₃ :
  Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)

Tactic:
rw [← lie_skew x y, map_neg, LinearMap.neg_apply]

Premises used: LinearMap.neg_apply, map_neg, lie_skew
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw rw₁ :
  Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
⊢ Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)

Tactic:
rw [traceForm_apply_lie_apply]

Premises used: LieModule.traceForm_apply_lie_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x y z : L
rw :
  Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) (-⁅y, x⁆) : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₁ :
  Eq.{u_1 + 1} (α := R) (((-(traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₂ :
  Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅y, x⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
rw₃ rw₄ :
  Eq.{u_1 + 1} (α := R) (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)
⊢ Eq.{u_1 + 1} (α := R) ((((traceForm R L M : (a : L) → L →ₗ[R] R) ⁅x, y⁆ : L →ₗ[R] R) : (a : L) → R) z : R)
    (-(((traceForm R L M : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) ⁅x, z⁆ : R)

Tactic:
rw [← lie_skew, map_neg, LinearMap.neg_apply, LieModule.traceForm_apply_lie_apply R L M]

Premises used: LinearMap.neg_apply, map_neg, lie_skew, LieModule.traceForm_apply_lie_apply
-- Module: Mathlib.Algebra.Lie.TraceForm
Goal:
R : Type u_1
L : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : AddCommGroup M
inst_4 : Module R M
inst_5 : LieRingModule L M
inst_6 : LieModule R L M
x : L
H :
  ∀ (y z : L),
    Eq.{u_1 + 1} (α := R) ((((⁅x, traceForm R L M⁆ : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
      ((((0 : (a : L) → L →ₗ[R] R) y : L →ₗ[R] R) : (a : L) → R) z : R)
⊢ Eq (α := LinearMap.BilinForm R L) ⁅x, traceForm R L M⁆ 0

Tactic:
ext y z