σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) = n
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ MvPolynomial.totalDegree φ = n
rw [totalDegree]
case a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) ≤ n

case a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) = n
apply le_antisymm
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) ≤ n
case a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ (Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e) ≤ n
apply Finset.sup_le
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ (Finsupp.sum d fun x e => e) ≤ n
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ ∀ (b : σ →₀ ℕ), b ∈ support φ → (Finsupp.sum b fun x e => e) ≤ n
intro d hd
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (Finsupp.sum d fun x e => e) ≤ n
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ support φ
⊢ (Finsupp.sum d fun x e => e) ≤ n
rw [mem_support_iff] at hd
no goals
case a.a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ (Finsupp.sum d fun x e => e) ≤ n
rw [Finsupp.sum, hφ hd]
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
case a
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
obtain ⟨d, hd⟩ : ∃ d, coeff d φ ≠ 0 := exists_coeff_ne_zero h
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ n ≤ Finset.sup (support φ) fun s => Finsupp.sum s fun x e => e
simp only [← hφ hd, Finsupp.sum]
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : coeff d φ ≠ 0
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
replace hd := Finsupp.mem_support_iff.mpr hd
no goals
case a.intro
σ : Type u_1
τ : Type ?u.163982
R : Type u_2
S : Type ?u.163988
inst✝ : CommSemiring R
φ ψ : MvPolynomial σ R
m n : ℕ
hφ : IsHomogeneous φ n
h : φ ≠ 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ ∑ x in d.support, ↑d x ≤ Finset.sup (support φ) fun s => ∑ x in s.support, ↑s x
exact Finset.le_sup (f := fun s ↦ ∑ x in s.support, (⇑s) x) hd