-- 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
h :
  ∀ (x : M),
    Eq (α := SymmetricAlgebra R M ⊗[R] R)
      (((↑(AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
                      (Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv :
                        SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R)
                      ((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] R) :
                [inst_3 :
                    FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (SymmetricAlgebra R M)
                      (SymmetricAlgebra R M ⊗[R] R)] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (RingHom.id R)
                        (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] R)] →
                    SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] R) ∘ₗ
              ι R M :
            (a : M) → SymmetricAlgebra R M ⊗[R] R)
          x :
        SymmetricAlgebra R M ⊗[R] R)
      (((↑((↑(AlgEquiv.symm (Algebra.TensorProduct.rid R R (SymmetricAlgebra R M))) :
                      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
                    SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
                [inst_3 :
                    FunLike (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (SymmetricAlgebra R M)
                      (SymmetricAlgebra R M ⊗[R] R)] →
                  [SemilinearMapClass (SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) (RingHom.id R)
                        (SymmetricAlgebra R M) (SymmetricAlgebra R M ⊗[R] R)] →
                    SymmetricAlgebra R M →ₗ[R] SymmetricAlgebra R M ⊗[R] R) ∘ₗ
              ι R M :
            (a : M) → SymmetricAlgebra R M ⊗[R] R)
          x :
        SymmetricAlgebra R M ⊗[R] R)
⊢ Eq (α := SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R)
    (AlgHom.comp (B := SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M)
        (Algebra.TensorProduct.map (AlgHom.id R (SymmetricAlgebra R M)) algebraMapInv :
          SymmetricAlgebra R M ⊗[R] SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R)
        ((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] R)
    ((↑(AlgEquiv.symm (Algebra.TensorProduct.rid R R (SymmetricAlgebra R M))) :
        SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R) :
      SymmetricAlgebra R M →ₐ[R] SymmetricAlgebra R M ⊗[R] R)

Tactic:
ext x