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