rw [homogenization, homogenization, homogenization, totalDegree_mul_eq hp hq, ←
  Finsupp.sum_single p, ← Finsupp.sum_single q, Finsupp.mapDomain_sum, Finsupp.mapDomain_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
⊢ homogenization i (p * q) = homogenization i p * homogenization i q
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)