-- 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] 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)
have 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)
Tactic: ext x