α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD (lookup a l) 0 = x ↔ x ∈ lookup a l
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ ↑(lookupFinsupp l) a = x ↔ x ∈ lookup a l
rw [lookupFinsupp_apply]
no goals
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
l : AList fun _x => M
a : α
x : M
hx : x ≠ 0
⊢ Option.getD (lookup a l) 0 = x ↔ x ∈ lookup a l
cases' lookup a l with m <;> simp [hx.symm]