no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.284872
r : R
e : ℕ
n✝ m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
n : σ
f : MvPolynomial σ R
d : ℕ
h : 0 < d
⊢ degreeOf n f < d ↔ ∀ (m : σ →₀ ℕ), m ∈ support f → ↑m n < d
rwa [degreeOf_eq_sup n f, Finset.sup_lt_iff]