apply IsHomogeneous.mul <;> simp [isHomogeneous_leadingTerms]
case hφ
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ (p.leadingTerms * q.leadingTerms).IsHomogeneous (p.leadingTerms.totalDegree + q.leadingTerms.totalDegree)

case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0
case h
R : Type ?u.191921
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
hp : p ≠ 0
hq : q ≠ 0
⊢ p.leadingTerms * q.leadingTerms ≠ 0