case zero
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
⊢ coeff (↑Nat.zero) 0 = ↑Nat.zero

case succ
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n : ℕ
ih : coeff (↑n) 0 = ↑n
⊢ coeff (↑(Nat.succ n)) 0 = ↑(Nat.succ n)
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
n : ℕ
R : Type u_1
inst✝ : Semiring R
⊢ coeff (↑n) 0 = ↑n
induction' n with n ih
no goals
case zero
R✝ : Type u
S : Type v
a b : R✝
n m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
⊢ coeff (↑Nat.zero) 0 = ↑Nat.zero
simp
no goals
case succ
R✝ : Type u
S : Type v
a b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p q r : R✝[X]
R : Type u_1
inst✝ : Semiring R
n : ℕ
ih : coeff (↑n) 0 = ↑n
⊢ coeff (↑(Nat.succ n)) 0 = ↑(Nat.succ n)
simp [ih]