no goals
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f✝ g✝ f g : Π₀ (a : α), N a
a : α
⊢ a ∈ neLocus f g ↔ ↑f a ≠ ↑g a
simpa only [neLocus, Finset.mem_filter, Finset.mem_union, mem_support_iff,
  and_iff_right_iff_imp] using Ne.ne_or_ne _