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 (p * X) r = comp p r * r
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, add_mul, add_comp]
| h_monomial n b =>
  simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]
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 (p * X) r = comp p r * r
hq : comp (q * X) r = comp q r * r
⊢ comp ((p + q) * X) r = comp (p + q) r * r
simp only [hp, hq, add_mul, add_comp]
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 (↑(monomial n) b * X) r = comp (↑(monomial n) b) r * r
simp only [pow_succ', mul_assoc, monomial_mul_X, monomial_comp]