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]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ↑Nat.zero = ↑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]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑(Nat.succ n) = ↑(Nat.succ n)
R : Type u
S : Type v
T : Type w
ι : Type y
a b : R
m n✝ : ℕ
inst✝¹ : Semiring R
p q r : R[X]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
⊢ eval₂ f x ↑n = ↑n
induction' n with n 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]
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x ↑Nat.zero = ↑Nat.zero
simp only [eval₂_zero, Nat.cast_zero, Nat.zero_eq]
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]
inst✝ : Semiring S
f : R →+* S
x : S
n : ℕ
ih : eval₂ f x ↑n = ↑n
⊢ eval₂ f x ↑(Nat.succ n) = ↑(Nat.succ n)
rw [n.cast_succ, eval₂_add, ih, eval₂_one, n.cast_succ]