no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
classical
simp only [← AList.insert_empty, insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]
no goals
α : Type u_1
M : Type u_2
inst✝ : Zero M
a : α
m : M
⊢ lookupFinsupp (singleton a m) = Finsupp.single a m
simp only [← AList.insert_empty, insert_lookupFinsupp, empty_lookupFinsupp, Finsupp.zero_update]