rw [← totalDegree_leadingTerms, ← totalDegree_leadingTerms p, ← totalDegree_leadingTerms q,
  leadingTerms_mul, IsHomogeneous.totalDegree]
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 * q).totalDegree = p.totalDegree + q.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).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