∀ {α : Type u_1} {β : Type u_2} {M : Type u_3} [inst : Zero M] (f : α × β →₀ M) (a : α),
  a ∈ Finset.image Prod.fst f.support ↔
    { support := Finset.filterMap (fun x => if x.1 = a then some x.2 else none) f.support ⋯, toFun := fun b => f (a, b),
        mem_support_toFun := ⋯ } ≠
      0