erw [Finsupp.mapDomain_single]
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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i (p.totalDegree + q.totalDegree - j.sum fun x m => m))
      ((monomial (a.1 + a.2)) (p a.1 * q a.2)) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.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
a : (ι →₀ ℕ) × (ι →₀ ℕ)
ha : a.1 ∈ p.support ∧ a.2 ∈ q.support
⊢ Finsupp.single (a.1 + a.2 + Finsupp.single i (p.totalDegree + q.totalDegree - (a.1 + a.2).sum fun x m => m))
      (p a.1 * q a.2) =
    (monomial
        (a.1 + Finsupp.single i (p.totalDegree - a.1.sum fun x m => m) +
          (a.2 + Finsupp.single i (q.totalDegree - a.2.sum fun x m => m))))
      (p a.1 * q a.2)