∀ {R : Type u} {σ : Type v} [inst : CommSemiring R] {τ : Type u_1} {f : σ → τ},
  Function.Injective f →
    ∀ (x : σ) (p : MvPolynomial σ R),
      (MvPolynomial.pderiv (f x)) ((MvPolynomial.rename f) p) = (MvPolynomial.rename f) ((MvPolynomial.pderiv x) p)