intro i
case neg.e_a.h_add
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
⊢ ∀ a_1 ∈ a.1.support ∪ a.2.support, ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂
case neg.e_a.h_add
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
i : ι
⊢ i ∈ a.1.support ∪ a.2.support → ∀ (b₁ b₂ : ℕ), b₁ + b₂ = b₁ + b₂