rfl
case h.e'_3
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
j : ι
this : ∀ {f s p q fs ss : ℕ}, fs ≤ p → ss ≤ q → f + s + (p + q - (fs + ss)) = f + (p - fs) + (s + (q - ss))
h : i = j
⊢ (a.2.sum fun x m => m) = a.2.sum fun x e => e
no goals