R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ ↑(weightedDegree' w) d = ⊥
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
⊢ IsWeightedHomogeneous w p ⊥
intro d hd
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
⊢ ↑(weightedDegree' w) d = ⊥
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ ↑(weightedDegree' w) d = ⊥
have h := weightedTotalDegree_coe w p (MvPolynomial.ne_zero_iff.mpr ⟨d, hd⟩)
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : (sup (support p) fun s => ↑(↑(weightedDegree' w) s)) = ↑⊥
⊢ ↑(weightedDegree' w) d = ⊥
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : weightedTotalDegree' w p = ↑(weightedTotalDegree w p)
⊢ ↑(weightedDegree' w) d = ⊥
simp only [weightedTotalDegree', hp] at h
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : (sup (support p) fun s => ↑(↑(weightedDegree' w) s)) = ↑⊥
⊢ ↑(↑(weightedDegree' w) d) ≤ sup (support p) fun s => ↑(↑(weightedDegree' w) s)
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : (sup (support p) fun s => ↑(↑(weightedDegree' w) s)) = ↑⊥
⊢ ↑(weightedDegree' w) d = ⊥
rw [eq_bot_iff, ← WithBot.coe_le_coe, ← h]
no goals
R : Type u_3
M : Type u_1
inst✝³ : CommSemiring R
σ : Type u_2
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
h : (sup (support p) fun s => ↑(↑(weightedDegree' w) s)) = ↑⊥
⊢ ↑(↑(weightedDegree' w) d) ≤ sup (support p) fun s => ↑(↑(weightedDegree' w) s)
apply Finset.le_sup (mem_support_iff.mpr hd)