case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : totalDegree φ < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : totalDegree φ < n
⊢ ↑(homogeneousComponent n) φ = 0
apply homogeneousComponent_eq_zero'
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n

case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : (sup (support φ) fun s => Finsupp.sum s fun x e => e) < n
⊢ ⊥ < n
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : totalDegree φ < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
rw [totalDegree, Finset.sup_lt_iff] at h
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ ∑ i in d.support, ↑d i ≠ n
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
⊢ ∀ (d : σ →₀ ℕ), d ∈ support φ → ∑ i in d.support, ↑d i ≠ n
intro d hd
no goals
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) < n
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ ∑ i in d.support, ↑d i ≠ n
exact ne_of_lt (h d hd)
no goals
case h
σ : Type u_2
τ : Type ?u.358984
R : Type u_1
S : Type ?u.358990
inst✝ : CommSemiring R
n : ℕ
φ ψ : MvPolynomial σ R
h : (sup (support φ) fun s => Finsupp.sum s fun x e => e) < n
⊢ ⊥ < n
exact lt_of_le_of_lt (Nat.zero_le _) h