∀ (R : Type u) [inst : CommSemiring R] {σ : Type u_1} (A : Type u_4) [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  (↑(AlgEquiv.restrictScalars R (MvPolynomial.algebraTensorAlgEquiv R A).symm)).comp
      (MvPolynomial.mapAlgHom (Algebra.ofId R A)) =
    Algebra.TensorProduct.includeRight