no goals
α : Type u_3
M : Type u_2
N : Type u_1
P : Type ?u.8114
inst✝⁴ : DecidableEq α
inst✝³ : DecidableEq N
inst✝² : Zero N
inst✝¹ : DecidableEq M
inst✝ : Zero M
f g : α →₀ N
F : N → M
F0 : F 0 = 0
x : α
⊢ x ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) → x ∈ neLocus f g
simpa only [mem_neLocus, mapRange_apply, not_imp_not] using congr_arg F