convert Finsupp.mapDomain_single (M := R) using 1
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
c : R
⊢ Finsupp.mapDomain (fun j => j + Finsupp.single i 0) (C c) = C c
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