case h
ι : Type u_1
R : Type ?u.953
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ ↑(toDfinsupp (single i m)) i✝ = ↑(Dfinsupp.single i m) i✝
ι : Type u_1
R : Type ?u.953
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ toDfinsupp (single i m) = Dfinsupp.single i m
ext
no goals
case h
ι : Type u_1
R : Type ?u.953
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ ↑(toDfinsupp (single i m)) i✝ = ↑(Dfinsupp.single i m) i✝
simp [Finsupp.single_apply, Dfinsupp.single_apply]