-- 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 : AddCommGroup A
inst_4 : DistribSMul A R
inst_5 : SMulCommClass A R R
Φ : LinearMap.BilinForm R L
x y : loopAlgebra R A L
a :
  ∀ (x_1 : A) (x_2 : L),
    Eq.{u_1 + 1} (α := R)
      ((((TensorProduct.AlgebraTensorModule.curry
                      {
                        toFun := fun (g : loopAlgebra R A L) ↦
                          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                            HSMul.hSMul (β := R) a
                              ((((Φ : (a : L) → L →ₗ[R] R)
                                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) (x + y) : A →₀ L) :
                                            (a : A) → L)
                                          (-a)) :
                                      L →ₗ[R] R) :
                                    (a : L) → R)
                                  v :
                                R),
                        map_add' := ⋯, map_smul' := ⋯ } ∘ₗ
                    AddMonoidAlgebra.lsingle x_1 :
                  R →ₗ[R] L →ₗ[R] R) :
                (a : R) → L →ₗ[R] R)
              1 :
            (a : L) → R)
          x_2 :
        R)
      ((((TensorProduct.AlgebraTensorModule.curry
                      (HAdd.hAdd (α := loopAlgebra R A L →ₗ[R] R)
                        {
                          toFun := fun (g : loopAlgebra R A L) ↦
                            sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                              HSMul.hSMul (β := R) a
                                ((((Φ : (a : L) → L →ₗ[R] R)
                                          ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) :
                                              (a : A) → L)
                                            (-a)) :
                                        L →ₗ[R] R) :
                                      (a : L) → R)
                                    v :
                                  R),
                          map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }
                        {
                          toFun := fun (g : loopAlgebra R A L) ↦
                            sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
                              HSMul.hSMul (β := R) a
                                ((((Φ : (a : L) → L →ₗ[R] R)
                                          ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) :
                                              (a : A) → L)
                                            (-a)) :
                                        L →ₗ[R] R) :
                                      (a : L) → R)
                                    v :
                                  R),
                          map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }) ∘ₗ
                    AddMonoidAlgebra.lsingle x_1 :
                  R →ₗ[R] L →ₗ[R] R) :
                (a : R) → L →ₗ[R] R)
              1 :
            (a : L) → R)
          x_2 :
        R)
⊢ {
      toFun := fun (g : loopAlgebra R A L) ↦
        sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
          HSMul.hSMul (β := R) a
            ((((Φ : (a : L) → L →ₗ[R] R)
                      ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) (x + y) : A →₀ L) : (a : A) → L) (-a)) :
                    L →ₗ[R] R) :
                  (a : L) → R)
                v :
              R),
      map_add' := ⋯, map_smul' := ⋯ } =
    HAdd.hAdd (α := loopAlgebra R A L →ₗ[R] R)
      {
        toFun := fun (g : loopAlgebra R A L) ↦
          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
            HSMul.hSMul (β := R) a
              ((((Φ : (a : L) → L →ₗ[R] R)
                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) x : A →₀ L) : (a : A) → L) (-a)) :
                      L →ₗ[R] R) :
                    (a : L) → R)
                  v :
                R),
        map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }
      {
        toFun := fun (g : loopAlgebra R A L) ↦
          sum ((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) g) fun (a : A) (v : L) ↦
            HSMul.hSMul (β := R) a
              ((((Φ : (a : L) → L →ₗ[R] R)
                        ((((toFinsupp R A L : (a : loopAlgebra R A L) → A →₀ L) y : A →₀ L) : (a : A) → L) (-a)) :
                      L →ₗ[R] R) :
                    (a : L) → R)
                  v :
                R),
        map_add' := ⋯, map_smul' := ⋯ : loopAlgebra R A L →ₗ[R] R }

Tactic:
ext