case zero
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 ^ Nat.zero) r = comp p r * r ^ Nat.zero

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
ih : comp (p * X ^ k) r = comp p r * r ^ k
⊢ comp (p * X ^ Nat.succ k) r = comp p r * r ^ Nat.succ k
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
⊢ comp (p * X ^ k) r = comp p r * r ^ k
induction' k with k ih
no goals
case zero
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 ^ Nat.zero) r = comp p r * r ^ Nat.zero
simp
no goals
case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝ : Semiring R
p q r : R[X]
k : ℕ
ih : comp (p * X ^ k) r = comp p r * r ^ k
⊢ comp (p * X ^ Nat.succ k) r = comp p r * r ^ Nat.succ k
simp [ih, pow_succ', ← mul_assoc, mul_X_comp]