case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
⊢ lookupFinsupp (insert a m l) = Finsupp.update (lookupFinsupp l) a m
ext b
no goals
case h
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
m : M
b : α
⊢ ↑(lookupFinsupp (insert a m l)) b = ↑(Finsupp.update (lookupFinsupp l) a m) b
by_cases h : b = a <;> simp [h]