R : Type u
S : Type ?u.77804
inst✝ : Ring R
i : ℕ
⊢ (if 0 = i then 1 else 0) = ↑(if 0 = i then 1 else 0)
R : Type u
S : Type ?u.77804
inst✝ : Ring R
i : ℕ
⊢ ↑(coeff (restriction 1) i) = ↑(coeff 1 i)
rw [coeff_restriction', coeff_one, coeff_one]
no goals
R : Type u
S : Type ?u.77804
inst✝ : Ring R
i : ℕ
⊢ (if 0 = i then 1 else 0) = ↑(if 0 = i then 1 else 0)
split_ifs <;> rfl