Theorem: MvPolynomial.leadingTerms_add_of_totalDegree_lt (FltRegular/ReadyForMathlib/Homogenization.lean)

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