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