no goals
α : Type u_1
M : Type ?u.4833
N : Type u_2
P : Type ?u.4839
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : Zero N
f g : α →₀ N
⊢ neLocus f g = neLocus g f
simp_rw [neLocus, Finset.union_comm, ne_comm]