no goals
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s t : σ
⊢ ↑(coeff R (single t 1)) (X s) = if t = s then 1 else 0
simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]