R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : ∃ a, ↑a = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : p ≠ 0
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
rw [Ne.def, ← weightedTotalDegree'_eq_bot_iff w p, ← Ne.def, WithBot.ne_bot_iff_exists] at hp
case intro
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : ∃ a, ↑a = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
obtain ⟨m, hm⟩ := hp
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p ≤ ↑(weightedTotalDegree w p)

case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ↑(weightedTotalDegree w p) ≤ weightedTotalDegree' w p
case intro
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
apply le_antisymm
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → ↑(weightedDegree' w) b ≤ sup (support p) fun s => ↑(weightedDegree' w) s
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ weightedTotalDegree' w p ≤ ↑(weightedTotalDegree w p)
simp only [weightedTotalDegree, weightedTotalDegree', Finset.sup_le_iff, WithBot.coe_le_coe]
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
b : σ →₀ ℕ
⊢ b ∈ support p → ↑(weightedDegree' w) b ≤ sup (support p) fun s => ↑(weightedDegree' w) s
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ∀ (b : σ →₀ ℕ), b ∈ support p → ↑(weightedDegree' w) b ≤ sup (support p) fun s => ↑(weightedDegree' w) s
intro b
no goals
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
b : σ →₀ ℕ
⊢ b ∈ support p → ↑(weightedDegree' w) b ≤ sup (support p) fun s => ↑(weightedDegree' w) s
exact Finset.le_sup
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ weightedTotalDegree' w p
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ↑(weightedTotalDegree w p) ≤ weightedTotalDegree' w p
simp only [weightedTotalDegree]
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ weightedTotalDegree' w p
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ weightedTotalDegree' w p
have hm' : weightedTotalDegree' w p ≤ m := le_of_eq hm.symm
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ ↑m
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ weightedTotalDegree' w p
rw [← hm]
no goals
case intro.a
R : Type u_2
M : Type u_3
inst✝³ : CommSemiring R
σ : Type u_1
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
m : M
hm : ↑m = weightedTotalDegree' w p
hm' : weightedTotalDegree' w p ≤ ↑m
⊢ ↑(sup (support p) fun s => ↑(weightedDegree' w) s) ≤ ↑m
simpa [weightedTotalDegree'] using hm'