case h
ι : Type u_1
R : Type ?u.8500
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ ↑(toFinsupp (single i m)) a✝ = ↑(Finsupp.single i m) a✝
ι : Type u_1
R : Type ?u.8500
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ toFinsupp (single i m) = Finsupp.single i m
ext
no goals
case h
ι : Type u_1
R : Type ?u.8500
M : Type u_2
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ ↑(toFinsupp (single i m)) a✝ = ↑(Finsupp.single i m) a✝
simp [Finsupp.single_apply, Dfinsupp.single_apply]