-- Module: Mathlib.Algebra.Lie.Loop
Goal:
R : Type u_1
A : Type u_2
L : Type u_3
inst : CommRing R
inst_1 : LieRing L
inst_2 : LieAlgebra R L
inst_3 : CommRing A
inst_4 : IsAddTorsionFree R
inst_5 : Algebra A R
Φ : LinearMap.BilinForm R L
hΦ : LinearMap.BilinForm.lieInvariant L Φ
hΦs : Φ.IsSymm
a : A
x : L
b : A
y : L
c : A
z : L
a₁ :
  HSMul.hSMul (β := R) b
      ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + c) ⁅x, z⁆ : (a : A) → L) (-b)) : L →ₗ[R] R) : (a : L) → R) y :
        R) =
    HSMul.hSMul (β := R) c
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (a + b) ⁅x, y⁆ : (a : A) → L) (-c)) : L →ₗ[R] R) : (a : L) → R)
            z :
          R) +
      HSMul.hSMul (β := R) a
        ((((Φ : (a : L) → L →ₗ[R] R) ((Finsupp.single (b + c) ⁅y, z⁆ : (a : A) → L) (-a)) : L →ₗ[R] R) : (a : L) → R)
            x :
          R)
⊢ Eq.{u_1 + 1} (α := TrivialLieModule R (loopAlgebra R A L) R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((((TensorProduct.AlgebraTensorModule.curry
                                  ((((TensorProduct.AlgebraTensorModule.curry
                                                ((Cohomology.d₂₃ R (loopAlgebra R A L)
                                                      (TrivialLieModule R (loopAlgebra R A L) R) :
                                                    (a :
                                                        ↥(Cohomology.twoCochain R (loopAlgebra R A L)
                                                            (TrivialLieModule R (loopAlgebra R A L) R))) →
                                                      loopAlgebra R A L →ₗ[R]
                                                        loopAlgebra R A L →ₗ[R]
                                                          loopAlgebra R A L →ₗ[R]
                                                            TrivialLieModule R (loopAlgebra R A L) R)
                                                  (twoCochainOfBilinear R A L Φ hΦs)) ∘ₗ
                                              AddMonoidAlgebra.lsingle a :
                                            R →ₗ[R]
                                              L →ₗ[R]
                                                loopAlgebra R A L →ₗ[R]
                                                  loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                                          (a : R) →
                                            L →ₗ[R]
                                              loopAlgebra R A L →ₗ[R]
                                                loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                                        1 :
                                      (a : L) →
                                        loopAlgebra R A L →ₗ[R]
                                          loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                                    x) ∘ₗ
                                AddMonoidAlgebra.lsingle b :
                              R →ₗ[R] L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                            (a : R) → L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                          1 :
                        (a : L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                      y) ∘ₗ
                  AddMonoidAlgebra.lsingle c :
                R →ₗ[R] L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
              (a : R) → L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
            1 :
          (a : L) → TrivialLieModule R (loopAlgebra R A L) R)
        z :
      TrivialLieModule R (loopAlgebra R A L) R)
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((((TensorProduct.AlgebraTensorModule.curry
                                  ((((TensorProduct.AlgebraTensorModule.curry 0 ∘ₗ AddMonoidAlgebra.lsingle a :
                                            R →ₗ[R]
                                              L →ₗ[R]
                                                loopAlgebra R A L →ₗ[R]
                                                  loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                                          (a : R) →
                                            L →ₗ[R]
                                              loopAlgebra R A L →ₗ[R]
                                                loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                                        1 :
                                      (a : L) →
                                        loopAlgebra R A L →ₗ[R]
                                          loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                                    x) ∘ₗ
                                AddMonoidAlgebra.lsingle b :
                              R →ₗ[R] L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
                            (a : R) → L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                          1 :
                        (a : L) → loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
                      y) ∘ₗ
                  AddMonoidAlgebra.lsingle c :
                R →ₗ[R] L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R) :
              (a : R) → L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
            1 :
          (a : L) → TrivialLieModule R (loopAlgebra R A L) R)
        z :
      TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
suffices
        b • Φ (Finsupp.single (a + c) ⁅x, z⁆ (-b)) y =
        c • Φ (Finsupp.single (a + b) ⁅x, y⁆ (-c)) z +
        a • Φ (Finsupp.single (b + c) ⁅y, z⁆ (-a)) x by
      simpa [trivial_lie_zero, sub_eq_zero, neg_add_eq_iff_eq_add, ← LinearEquiv.map_add,
        -LinearEquiv.map_add]