α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = Option.getD (lookup a l) 0
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ ↑(lookupFinsupp l) a = Option.getD (lookup a l) 0
simp only [lookupFinsupp, ne_eq, Finsupp.coe_mk]
no goals
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
⊢ Option.getD (lookup a l) 0 = Option.getD (lookup a l) 0
congr