-- 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 : A) (x : L) (b : A) (y : L) (c : A) (z : L),
    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)
⊢ Eq (α :=
    loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
    ((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) :
      loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)
    (0 :
      loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] loopAlgebra R A L →ₗ[R] TrivialLieModule R (loopAlgebra R A L) R)

Tactic:
ext a x b y c z