R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ↑(weightedDegree' w) c = m
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
⊢ IsWeightedHomogeneous w (↑(monomial d) r) m
intro c hc
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
hc : (if d = c then r else 0) ≠ 0
⊢ ↑(weightedDegree' w) c = m
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ↑(weightedDegree' w) c = m
rw [coeff_monomial] at hc
case inl
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : d = c
hc : r ≠ 0
⊢ ↑(weightedDegree' w) c = m

case inr
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : ¬d = c
hc : 0 ≠ 0
⊢ ↑(weightedDegree' w) c = m
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
hc : (if d = c then r else 0) ≠ 0
⊢ ↑(weightedDegree' w) c = m
split_ifs at hc with h
case inl
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
hc✝ : r ≠ 0
hc : coeff d (↑(monomial d) r) ≠ 0
⊢ ↑(weightedDegree' w) d = m
case inl
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : d = c
hc : r ≠ 0
⊢ ↑(weightedDegree' w) c = m
subst c
no goals
case inl
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
hc✝ : r ≠ 0
hc : coeff d (↑(monomial d) r) ≠ 0
⊢ ↑(weightedDegree' w) d = m
exact hm
no goals
case inr
R : Type u_3
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_1
inst✝ : AddCommMonoid M
w : σ → M
d : σ →₀ ℕ
r : R
m : M
hm : ↑(weightedDegree' w) d = m
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : ¬d = c
hc : 0 ≠ 0
⊢ ↑(weightedDegree' w) c = m
contradiction