case a
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ List.toFinset (AList.keys (toAList f)) ↔ a✝ ∈ f.support
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
⊢ List.toFinset (AList.keys (toAList f)) = f.support
ext
no goals
case a
α : Type u_1
M : Type u_2
inst✝¹ : Zero M
inst✝ : DecidableEq α
f : α →₀ M
a✝ : α
⊢ a✝ ∈ List.toFinset (AList.keys (toAList f)) ↔ a✝ ∈ f.support
simp [toAList, AList.mem_keys, AList.keys, List.keys]