σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
⊢ IsHomogeneous (↑(monomial d) r) n
intro c hc
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
hc : (if d = c then r else 0) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc : coeff c (↑(monomial d) r) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
rw [coeff_monomial] at hc
case inl
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : d = c
hc : r ≠ 0
⊢ ∑ i in c.support, ↑c i = n

case inr
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : ¬d = c
hc : 0 ≠ 0
⊢ ∑ i in c.support, ↑c i = n
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
hc : (if d = c then r else 0) ≠ 0
⊢ ∑ i in c.support, ↑c i = n
split_ifs at hc with h
case inl
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
hc✝ : r ≠ 0
hc : coeff d (↑(monomial d) r) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
case inl
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : d = c
hc : r ≠ 0
⊢ ∑ i in c.support, ↑c i = n
subst c
no goals
case inl
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
hc✝ : r ≠ 0
hc : coeff d (↑(monomial d) r) ≠ 0
⊢ ∑ i in d.support, ↑d i = n
exact hn
no goals
case inr
σ : Type u_1
τ : Type ?u.126597
R : Type u_2
S : Type ?u.126603
inst✝ : CommSemiring R
d : σ →₀ ℕ
r : R
n : ℕ
hn : ∑ i in d.support, ↑d i = n
c : σ →₀ ℕ
hc✝ : coeff c (↑(monomial d) r) ≠ 0
h : ¬d = c
hc : 0 ≠ 0
⊢ ∑ i in c.support, ↑c i = n
contradiction