rw [leadingTerms, leadingTerms, totalDegree_add_eq_left_of_totalDegree_lt h,
  LinearMap.map_add, homogeneousComponent_eq_zero _ q h, add_zero]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : q.totalDegree < p.totalDegree
⊢ (p + q).leadingTerms = p.leadingTerms
no goals