calc
  _ ≤ max (wp * (leadingTerms q)).totalDegree ((leadingTerms p) * wq + wp * wq).totalDegree :=
    totalDegree_add _ _
  _ ≤
      max (wp * (leadingTerms q)).totalDegree
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (le_refl _) (totalDegree_add _ _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p) * wq).totalDegree (wp * wq).totalDegree) :=
    (max_le_max (totalDegree_mul _ _) (le_refl _))
  _ ≤
      max (wp.totalDegree + (leadingTerms q).totalDegree)
        (max ((leadingTerms p).totalDegree + wq.totalDegree)
          (wp.totalDegree + wq.totalDegree)) :=
    (max_le_max (le_refl _) (max_le_max (totalDegree_mul _ _) (totalDegree_mul _ _)))
  _ < p.totalDegree + q.totalDegree := ?_
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ (wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).totalDegree < p.totalDegree + q.totalDegree
case neg.intro.intro.intro.intro.h
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp✝ : ¬p.totalDegree = 0
hq✝ : ¬q.totalDegree = 0
this : (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
wp : MvPolynomial ι S
hp : p = p.leadingTerms + wp
tp : wp.totalDegree < p.totalDegree
wq : MvPolynomial ι S
hq : q = q.leadingTerms + wq
tq : wq.totalDegree < q.totalDegree
⊢ max (wp.totalDegree + q.leadingTerms.totalDegree)
      (max (p.leadingTerms.totalDegree + wq.totalDegree) (wp.totalDegree + wq.totalDegree)) <
    p.totalDegree + q.totalDegree