-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem isWeightedHomogeneous_of_total_degree_zero [SemilatticeSup M] [OrderBot M] (w : σ → M)
    {p : MvPolynomial σ R} (hp : weightedTotalDegree w p = (⊥ : M)) :
    IsWeightedHomogeneous w p (⊥ : M)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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 : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥
⊢ (weight w) d = ⊥

Tactic:
rw [eq_bot_iff, ← WithBot.coe_le_coe, ← h]

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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 : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥
⊢ ↑((weight w) d) ≤ p.support.sup fun s => ↑((weight w) s)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ (weight w) d = ⊥

Tactic:
have h := weightedTotalDegree_coe w p (MvPolynomial.ne_zero_iff.mpr ⟨d, hd⟩)

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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)
⊢ (weight w) d = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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)
⊢ (weight w) d = ⊥

Tactic:
simp only [weightedTotalDegree', hp] at h

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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 : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥
⊢ (weight w) d = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
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 : (p.support.sup fun s => ↑((weight w) s)) = ↑⊥
⊢ ↑((weight w) d) ≤ p.support.sup fun s => ↑((weight w) s)

Tactic:
apply Finset.le_sup (mem_support_iff.mpr hd)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
⊢ IsWeightedHomogeneous w p ⊥

Tactic:
intro d hd

Result:
R : Type u_1
M : Type u_2
inst✝³ : CommSemiring R
σ : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : SemilatticeSup M
inst✝ : OrderBot M
w : σ → M
p : MvPolynomial σ R
hp : weightedTotalDegree w p = ⊥
d : σ →₀ ℕ
hd : coeff d p ≠ 0
⊢ (weight w) d = ⊥