∀ {α : Type u_2} {β : Type u_3} {M : Type u_1} [inst : Zero M] (f : α ↪ β) (v : α →₀ M) (b : β)
  (h : ∃ a, v a ≠ 0 ∧ f a = b), (¬∃ a, f a = b) → v (Finset.choose (fun a₁ => f a₁ = b) v.support ⋯) = 0