[GOAL]
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(↑(traceForm R L M) ⁅x, y⁆) z = ↑(↑(traceForm R L M) x) ⁅y, z⁆
[PROOFSTEP]
calc
  traceForm R L M ⁅x, y⁆ z = trace R _ (φ ⁅x, y⁆ ∘ₗ φ z) := by simp only [traceForm_apply_apply]
  _ = trace R _ ((φ x * φ y - φ y * φ x) * φ z) := ?_
  _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ y * (φ x * φ z)) := ?_
  _ = trace R _ (φ x * (φ y * φ z)) - trace R _ (φ x * (φ z * φ y)) := ?_
  _ = traceForm R L M x ⁅y, z⁆ := ?_
[GOAL]
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(↑(traceForm R L M) ⁅x, y⁆) z = ↑(trace R M) (LinearMap.comp (↑φ ⁅x, y⁆) (↑φ z))
[PROOFSTEP]
simp only [traceForm_apply_apply]
[GOAL]
case calc_1
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (LinearMap.comp (↑φ ⁅x, y⁆) (↑φ z)) = ↑(trace R M) ((↑φ x * ↑φ y - ↑φ y * ↑φ x) * ↑φ z)
[PROOFSTEP]
simp only [LieHom.map_lie, Ring.lie_def, ← LinearMap.mul_eq_comp]
[GOAL]
case calc_2
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) ((↑φ x * ↑φ y - ↑φ y * ↑φ x) * ↑φ z) =
    ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ y * (↑φ x * ↑φ z))
[PROOFSTEP]
simp only [sub_mul, mul_sub, map_sub, mul_assoc]
[GOAL]
case calc_3
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ y * (↑φ x * ↑φ z)) =
    ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ x * (↑φ z * ↑φ y))
[PROOFSTEP]
simp only [LinearMap.trace_mul_cycle' R (φ x) (φ z) (φ y)]
[GOAL]
case calc_4
R : Type u_1
L : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : LieRing L
inst✝⁶ : LieAlgebra R L
M : Type u_3
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : LieRingModule L M
inst✝² : LieModule R L M
inst✝¹ : Module.Free R M
inst✝ : Module.Finite R M
x y z : L
⊢ ↑(trace R M) (↑φ x * (↑φ y * ↑φ z)) - ↑(trace R M) (↑φ x * (↑φ z * ↑φ y)) = ↑(↑(traceForm R L M) x) ⁅y, z⁆
[PROOFSTEP]
simp only [traceForm_apply_apply, LieHom.map_lie, Ring.lie_def, mul_sub, map_sub, ← LinearMap.mul_eq_comp]
