by_cases hp : p.totalDegree = 0
R : Type ?u.178489
ι : Type u_2
inst✝² : CommSemiring R
S : Type u_1
inst✝¹ : CommRing S
inst✝ : IsDomain S
p q : MvPolynomial ι S
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms
case pos
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
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms

case neg
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
⊢ (p * q).leadingTerms = p.leadingTerms * q.leadingTerms