simp only [Pi.add_apply, Finsupp.coe_add, Finsupp.coe_tsub, Pi.sub_apply]
case neg.e_a.h
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 : ι
⊢ (a.1 + a.2 +
        (Finsupp.single i p.totalDegree + Finsupp.single i q.totalDegree -
          (Finsupp.single i (a.1.sum fun x m => m) + Finsupp.single i (a.2.sum fun x m => m))))
      j =
    (a.1 + (Finsupp.single i p.totalDegree - Finsupp.single i (a.1.sum fun x m => m)) +
        (a.2 + (Finsupp.single i q.totalDegree - Finsupp.single i (a.2.sum fun x m => m))))
      j

case neg.e_a.h_zero
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, 0 = 0

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
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 : ι
⊢ a.1 j + a.2 j +
      ((Finsupp.single i p.totalDegree) j + (Finsupp.single i q.totalDegree) j -
        ((Finsupp.single i (a.1.sum fun x m => m)) j + (Finsupp.single i (a.2.sum fun x m => m)) j)) =
    a.1 j + ((Finsupp.single i p.totalDegree) j - (Finsupp.single i (a.1.sum fun x m => m)) j) +
      (a.2 j + ((Finsupp.single i q.totalDegree) j - (Finsupp.single i (a.2.sum fun x m => m)) j))

case neg.e_a.h_zero
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, 0 = 0

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₂