-- Module: Mathlib.RingTheory.Bialgebra.SymmetricAlgebra
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
x : M
w :
  Eq (α := SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
    (((TensorProduct.AlgebraTensorModule.assoc R R R (SymmetricAlgebra R M) (SymmetricAlgebra R M)
              (SymmetricAlgebra R M) :
            SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ≃ₗ[R]
              SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
          (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
            SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
        (((TensorProduct.AlgebraTensorModule.map
                (AlgHom.toLinearMap
                  ((lift :
                      (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                        SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                            (a : SymmetricAlgebra R M) →
                              SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          1 ∘ₗ
                        ι R M)
                      ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                            (a : SymmetricAlgebra R M) →
                              SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          1 ∘ₗ
                        ι R M))))
                LinearMap.id :
              SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R]
                SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
            (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
              SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          ((((lift :
                    (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)
                    ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)) :
                SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
              (a : RingQuot (TensorAlgebra.SymRel R M)) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
            ((RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M) :
                (a : TensorAlgebra R M) → RingQuot (TensorAlgebra.SymRel R M))
              ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)))) :
      SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (AlgHom.toLinearMap
                ((lift :
                    (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)
                    ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)))) :
            SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R]
              SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
          (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
            SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
        ((((lift :
                  (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                    SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                        (a : SymmetricAlgebra R M) →
                          SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      1 ∘ₗ
                    ι R M)
                  ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                        (a : SymmetricAlgebra R M) →
                          SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      1 ∘ₗ
                    ι R M)) :
              SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
            (a : RingQuot (TensorAlgebra.SymRel R M)) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          ((RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M) :
              (a : TensorAlgebra R M) → RingQuot (TensorAlgebra.SymRel R M))
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))) :
      SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
⊢ Eq (α := SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
    (((TensorProduct.AlgebraTensorModule.assoc R R R (SymmetricAlgebra R M) (SymmetricAlgebra R M)
              (SymmetricAlgebra R M) :
            SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ≃ₗ[R]
              SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
          (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
            SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
        (((TensorProduct.AlgebraTensorModule.map
                (AlgHom.toLinearMap
                  ((lift :
                      (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                        SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                            (a : SymmetricAlgebra R M) →
                              SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          1 ∘ₗ
                        ι R M)
                      ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                            (a : SymmetricAlgebra R M) →
                              SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          1 ∘ₗ
                        ι R M))))
                LinearMap.id :
              SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R]
                SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
            (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
              SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          ((((lift :
                    (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)
                    ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)) :
                SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
              (a : RingQuot (TensorAlgebra.SymRel R M)) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
            ((RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M) :
                (a : TensorAlgebra R M) → RingQuot (TensorAlgebra.SymRel R M))
              ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x)))) :
      SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
    (((TensorProduct.AlgebraTensorModule.map LinearMap.id
              (AlgHom.toLinearMap
                ((lift :
                    (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                    ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)
                    ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                          (a : SymmetricAlgebra R M) →
                            SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                        1 ∘ₗ
                      ι R M)))) :
            SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₗ[R]
              SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
          (a : SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
            SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
        ((((lift :
                  (a : M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) →
                    SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                (HAdd.hAdd (α := M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                  ((LinearMap.flip (TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) :
                        (a : SymmetricAlgebra R M) →
                          SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      1 ∘ₗ
                    ι R M)
                  ((TensorProduct.mk R (SymmetricAlgebra R M) (SymmetricAlgebra R M) :
                        (a : SymmetricAlgebra R M) →
                          SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      1 ∘ₗ
                    ι R M)) :
              SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
            (a : RingQuot (TensorAlgebra.SymRel R M)) → SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
          ((RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M) :
              (a : TensorAlgebra R M) → RingQuot (TensorAlgebra.SymRel R M))
            ((TensorAlgebra.ι R : (a : M) → TensorAlgebra R M) x))) :
      SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))

Tactic:
abel