erw [Finset.sum_mul_sum, Finset.sum_mul_sum, ← Finset.sum_product', ← Finset.sum_product']
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
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              j.sum fun x m => m))
      (Finsupp.sum p Finsupp.single * Finsupp.sum q Finsupp.single) =
    (Finsupp.sum p fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)) *
      Finsupp.sum q fun a b =>
        Finsupp.mapDomain
          (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
          (Finsupp.single a b)
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
            (totalDegree (Finsupp.sum p Finsupp.single) + totalDegree (Finsupp.sum q Finsupp.single) -
              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,
      (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum p Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.1 (p x.1) *
        (fun a b =>
            Finsupp.mapDomain
              (fun j => j + Finsupp.single i (totalDegree (Finsupp.sum q Finsupp.single) - j.sum fun x m => m))
              (Finsupp.single a b))
          x.2 (q x.2)