R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ (b : σ →₀ ℕ), b ∈ support f → (sum b fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0

R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : (Finset.sup (support f) fun s => sum s fun x e => e) < ∑ i in d.support, ↑d i
⊢ ⊥ < ∑ i in d.support, ↑d i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : totalDegree f < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
rw [totalDegree, Finset.sup_lt_iff] at h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ support f → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : ∀ (b : σ →₀ ℕ), b ∈ support f → (sum b fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
specialize h d
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : d ∈ support f → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
rw [mem_support_iff] at h
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ ¬(sum d fun x e => e) < ∑ i in d.support, ↑d i
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ coeff d f = 0
refine' not_not.mp (mt h _)
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : coeff d f ≠ 0 → (sum d fun x e => e) < ∑ i in d.support, ↑d i
⊢ ¬(sum d fun x e => e) < ∑ i in d.support, ↑d i
exact lt_irrefl _
no goals
R : Type u
S : Type v
σ : Type u_1
τ : Type ?u.477178
r : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝ : CommSemiring R
p q f : MvPolynomial σ R
d : σ →₀ ℕ
h : (Finset.sup (support f) fun s => sum s fun x e => e) < ∑ i in d.support, ↑d i
⊢ ⊥ < ∑ i in d.support, ↑d i
exact lt_of_le_of_lt (Nat.zero_le _) h