case zero
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
⊢ eval₂ f t ((comp p^[Nat.zero]) q) = ((fun x => eval₂ f x p)^[Nat.zero]) (eval₂ f t q)

case succ
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t ((comp p^[k]) q) = ((fun x => eval₂ f x p)^[k]) (eval₂ f t q)
⊢ eval₂ f t ((comp p^[Nat.succ k]) q) = ((fun x => eval₂ f x p)^[Nat.succ k]) (eval₂ f t q)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n : ℕ
inst✝¹ : Semiring R
p q : R[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
k : ℕ
t : S
⊢ eval₂ f t ((comp p^[k]) q) = ((fun x => eval₂ f x p)^[k]) (eval₂ f t q)
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[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
⊢ eval₂ f t ((comp p^[Nat.zero]) q) = ((fun x => eval₂ f x p)^[Nat.zero]) (eval₂ f t q)
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[X]
x : R
inst✝ : CommSemiring S
f : R →+* S
t : S
k : ℕ
IH : eval₂ f t ((comp p^[k]) q) = ((fun x => eval₂ f x p)^[k]) (eval₂ f t q)
⊢ eval₂ f t ((comp p^[Nat.succ k]) q) = ((fun x => eval₂ f x p)^[Nat.succ k]) (eval₂ f t q)
rw [Function.iterate_succ_apply', Function.iterate_succ_apply', eval₂_comp, IH]