-- 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
w :
  ∀ (x : M),
    Eq (α := SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
      (((AlgHom.toLinearMap
                  (AlgHom.comp (B := RingQuot (R := TensorAlgebra R M) (TensorAlgebra.SymRel R M))
                    (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      ((↑(Algebra.TensorProduct.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)) :
                        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R]
                          SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
                      (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                          (Algebra.TensorProduct.map
                              ((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)))
                              (AlgHom.id R (SymmetricAlgebra R M)) :
                            SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R]
                              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) :
                        SymmetricAlgebra R M →ₐ[R]
                          SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
                    (RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M))) ∘ₗ
                TensorAlgebra.ι R :
              M →ₗ[R] SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
            (a : M) → SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
          x :
        SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
      (((AlgHom.toLinearMap
                  (AlgHom.comp (B := RingQuot (R := TensorAlgebra R M) (TensorAlgebra.SymRel R M))
                    (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (Algebra.TensorProduct.map (AlgHom.id 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 ⊗[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))
                    (RingQuot.mkAlgHom R (TensorAlgebra.SymRel R M))) ∘ₗ
                TensorAlgebra.ι R :
              M →ₗ[R] SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)) :
            (a : M) → SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra 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 ⊗[R] SymmetricAlgebra R M))
    (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        ((↑(Algebra.TensorProduct.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)) :
          SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R]
            SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
        (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
            (Algebra.TensorProduct.map
                ((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)))
                (AlgHom.id R (SymmetricAlgebra R M)) :
              SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R]
                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) :
          SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M) :
      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))
    (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        (Algebra.TensorProduct.map (AlgHom.id 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 ⊗[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) :
      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] (SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M))

Tactic:
ext x