rw [add_assoc, leadingTerms_add_of_totalDegree_lt, leadingTerms_add_of_totalDegree_lt,
  leadingTerms_add_of_totalDegree_lt, leadingTerms_idempotent, leadingTerms_idempotent,
  leadingTerms_eq_self_iff_isHomogeneous]
case neg.intro.intro.intro.intro
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
⊢ (p.leadingTerms * q.leadingTerms + wp * q.leadingTerms + (p.leadingTerms * wq + wp * wq)).leadingTerms =
    (p.leadingTerms + wp).leadingTerms * (q.leadingTerms + wq).leadingTerms
case neg.intro.intro.intro.intro
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
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms * q.leadingTerms).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
⊢ wq.totalDegree < q.leadingTerms.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.totalDegree < p.leadingTerms.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.leadingTerms * q.leadingTerms).totalDegree