-- Lean 4 proof step from Mathlib.RingTheory.Bialgebra.SymmetricAlgebra (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module 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))
have 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))
Tactic: ext x