-- Module: Mathlib.Algebra.Polynomial.Module.TensorProduct
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
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)
⊢ (↑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

Tactic:
ext n x