R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ (b : Fin n →₀ ℕ),
    b ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i) → ↑b j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ degreeOf j (Polynomial.coeff (↑(finSuccEquiv R n) p) i) ≤ degreeOf (Fin.succ j) p
rw [degreeOf_eq_sup, degreeOf_eq_sup, Finset.sup_le_iff]
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑m j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
⊢ ∀ (b : Fin n →₀ ℕ),
    b ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i) → ↑b j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
intro m hm
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑(cons i m) (Fin.succ j) ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑m j ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
rw [← Finsupp.cons_succ j i m]
no goals
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type ?u.1382844
a a' a₁ a₂ : R
e : ℕ
s : σ →₀ ℕ
inst✝ : CommSemiring R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
j : Fin n
i : ℕ
m : Fin n →₀ ℕ
hm : m ∈ support (Polynomial.coeff (↑(finSuccEquiv R n) p) i)
⊢ ↑(cons i m) (Fin.succ j) ≤ Finset.sup (support p) fun m => ↑m (Fin.succ j)
exact Finset.le_sup
  (f := fun (g : Fin (Nat.succ n) →₀ ℕ) => g (Fin.succ j))
  (support_coeff_finSuccEquiv.1 hm)