rw [Finsupp.mapDomain_finset_sum]
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      (∑ x ∈ p.support ×ˢ q.support, Finsupp.single x.1 (p x.1) * Finsupp.single x.2 (q x.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))
case neg
R : Type ?u.198757
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
i : ι
p q : MvPolynomial ι S
hp : ¬p = 0
hq : ¬q = 0
⊢ ∑ i_1 ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
        (Finsupp.single i_1.1 (p i_1.1) * Finsupp.single i_1.2 (q i_1.2)) =
    ∑ x ∈ p.support ×ˢ q.support,
      Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.1 (p x.1)) *
        Finsupp.mapDomain (fun j => j + Finsupp.single i (q.totalDegree - j.sum fun x m => m))
          (Finsupp.single x.2 (q x.2))