R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310239
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ support f
⊢ ↑m i ≤ Finset.sup (support f) fun m => ↑m i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310239
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ support f
⊢ ↑m i ≤ degreeOf i f
rw [degreeOf_eq_sup i]
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.310239
r : R
e : ℕ
n m✝ : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q : MvPolynomial σ R
i : σ
f : MvPolynomial σ R
m : σ →₀ ℕ
h_m : m ∈ support f
⊢ ↑m i ≤ Finset.sup (support f) fun m => ↑m i
apply Finset.le_sup h_m