rw [IsHomogeneous.totalDegree]
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
⊢ (p.leadingTerms * q.leadingTerms).totalDegree = p.totalDegree + q.totalDegree
case 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
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.totalDegree + q.totalDegree)

case 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
⊢ p.leadingTerms * q.leadingTerms ≠ 0