no goals
α : Type u_1
M : Type ?u.28251
N : Type u_2
P : Type ?u.28257
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f f₁ f₂ g g₁ g₂ : α →₀ N
⊢ neLocus (f - g₁) (f - g₂) = neLocus g₁ g₂
simp only [sub_eq_add_neg, neLocus_add_left, neLocus_neg_neg]