rw [single_eq_monomial]
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = Finsupp.single (0 + Finsupp.single i 0) c
case h.e'_3
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ C c = (monomial (0 + Finsupp.single i 0)) c