rw [Finsupp.mapDomain_congr this]
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m)) p = p
case neg
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
hpn : ¬p = 0
hp : IsWeightedHomogeneous 1 p p.totalDegree
this : ∀ x ∈ p.support, (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun _x m => m)) x = x
⊢ Finsupp.mapDomain (fun x => x) p = p