-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Module.TensorProduct (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : LinearMap (R := R[X]) (RingHom.id R[X]) (R[X] ⊗[R] M) (PolynomialModule R M) := liftBaseChange R[X] (lsingle R 0)
inv : PolynomialModule R M →ₗ[R] R[X] ⊗[R] M :=
  (↑R :
        {S : Type u_1} →
          {M M₂ : Type (max u_1 u_2)} →
            [inst : Semiring R] →
              [inst_3 : Semiring S] →
                [inst_4 : AddCommMonoid M] →
                  [inst_5 : AddCommMonoid M₂] →
                    [inst_6 : Module R M] →
                      [inst_7 : Module R M₂] →
                        [inst_8 : Module S M] →
                          [inst_9 : Module S M₂] → [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
      (eval X) ∘ₗ
    map R[X] ((TensorProduct.mk R R[X] M : (a : R[X]) → M →ₗ[R] R[X] ⊗[R] M) 1)
left :
  inv ∘ₗ
      (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_3 : Semiring S] →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        e =
    LinearMap.id
⊢ (↑R :
          {S : Type u_1} →
            {M : Type (max u_1 u_2)} →
              {M₂ : Type u_2} →
                [inst : Semiring R] →
                  [inst_3 : Semiring S] →
                    [inst_4 : AddCommMonoid M] →
                      [inst_5 : AddCommMonoid M₂] →
                        [inst_6 : Module R M] →
                          [inst_7 : Module R M₂] →
                            [inst_8 : Module S M] →
                              [inst_9 : Module S M₂] →
                                [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
        e ∘ₗ
      inv =
    LinearMap.id
have h : ∀ (n : ℕ) (x : M),
  Eq (α := PolynomialModule R M)
    ((((↑R :
                  {S : Type u_1} →
                    {M : Type (max u_1 u_2)} →
                      {M₂ : Type u_2} →
                        [inst : Semiring R] →
                          [inst_3 : Semiring S] →
                            [inst_4 : AddCommMonoid M] →
                              [inst_5 : AddCommMonoid M₂] →
                                [inst_6 : Module R M] →
                                  [inst_7 : Module R M₂] →
                                    [inst_8 : Module S M] →
                                      [inst_9 : Module S M₂] →
                                        [LinearMap.CompatibleSMul M M₂ R S] → (fₗ : M →ₗ[S] M₂) → M →ₗ[R] M₂)
                e ∘ₗ
              inv) ∘ₗ
            lsingle R n :
          (a : M) → PolynomialModule R M)
        x :
      PolynomialModule R M)
    ((LinearMap.id ∘ₗ lsingle R n : (a : M) → PolynomialModule R M) x : PolynomialModule R M)
Tactic: ext n x