rw [Finset.inter_eq_left]
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p.leadingTerms.support ∩ p.support = p.leadingTerms.support
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this✝¹ : DecidableEq ι := Classical.decEq ι
this✝ : ∀ x ∈ p.leadingTerms.support, x.support.sum ⇑x = p.totalDegree
this : p.leadingTerms.support ⊆ p.support
⊢ p.leadingTerms.support ⊆ p.support