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 (X ^ Nat.zero) p = p ^ 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 (X ^ k) p = p ^ k
⊢ comp (X ^ Nat.succ k) p = p ^ 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 (X ^ k) p = p ^ 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 (X ^ Nat.zero) p = p ^ 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 (X ^ k) p = p ^ k
⊢ comp (X ^ Nat.succ k) p = p ^ Nat.succ k
simp [pow_succ', mul_X_comp, ih]