case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ coeff (update p n a) n✝ = coeff (p + ↑C (a - coeff p n) * X ^ n) n✝
R✝ : Type u
S : Type v
a✝ b : R✝
n✝ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
⊢ update p n a = p + ↑C (a - coeff p n) * X ^ n
ext
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else coeff p n✝) = coeff p n✝ + if n✝ = n then a - coeff p n else 0
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ coeff (update p n a) n✝ = coeff (p + ↑C (a - coeff p n) * X ^ n) n✝
rw [coeff_update_apply, coeff_add, coeff_C_mul_X_pow]
no goals
case a
R✝ : Type u
S : Type v
a✝ b : R✝
n✝¹ m : ℕ
inst✝¹ : Semiring R✝
p✝ q r : R✝[X]
R : Type u_1
inst✝ : Ring R
p : R[X]
n : ℕ
a : R
n✝ : ℕ
⊢ (if n✝ = n then a else coeff p n✝) = coeff p n✝ + if n✝ = n then a - coeff p n else 0
split_ifs with h <;> simp [h]