no goals
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
⊢ comp (↑C a * p) r = ↑C a * comp p r
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp [hp, hq, mul_add]
| h_monomial n b =>
  simp [mul_assoc]
no goals
case h_add
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p✝ q✝ r p q : R[X]
hp : comp (↑C a * p) r = ↑C a * comp p r
hq : comp (↑C a * q) r = ↑C a * comp q r
⊢ comp (↑C a * (p + q)) r = ↑C a * comp (p + q) r
simp [hp, hq, mul_add]
no goals
case h_monomial
R : Type u
S : Type v
T : Type w
ι : Type y
a b✝ : R
m n✝ : ℕ
inst✝ : Semiring R
p q r : R[X]
n : ℕ
b : R
⊢ comp (↑C a * ↑(monomial n) b) r = ↑C a * comp (↑(monomial n) b) r
simp [mul_assoc]