rw [(_ :
    (p.support.filter fun s : ι →₀ ℕ => ∑ i : ι in s.support, s i = p.totalDegree) =
      p.support)]
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ filter (fun d => ∑ i ∈ d.support, d i = p.totalDegree) p.support, (monomial d) (coeff d p) = p
case mpr
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ ∑ d ∈ p.support, (monomial d) (coeff d p) = p

R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
h : p.IsHomogeneous p.totalDegree
⊢ filter (fun s => ∑ i ∈ s.support, s i = p.totalDegree) p.support = p.support