no goals
α : Type u_1
M : Type ?u.2977
N : Type u_2
P : Type ?u.2983
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f✝ g✝ f g : α →₀ N
h : f = g
⊢ neLocus f f = ∅
simp only [neLocus, Ne.def, eq_self_iff_true, not_true, Finset.filter_False]