case pos
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
h : a = 0
⊢ sum (↑(monomial n) a) f = f n a

case neg
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
h : ¬a = 0
⊢ sum (↑(monomial n) a) f = f n a
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
⊢ sum (↑(monomial n) a) f = f n a
by_cases h : a = 0
no goals
case pos
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
h : a = 0
⊢ sum (↑(monomial n) a) f = f n a
simp [h, hf]
no goals
case neg
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q : R[X]
S : Type u_1
inst✝ : AddCommMonoid S
n : ℕ
a : R
f : ℕ → R → S
hf : f n 0 = 0
h : ¬a = 0
⊢ sum (↑(monomial n) a) f = f n a
simp [sum, support_monomial, h, coeff_monomial]