case a
α : Type u_4
M : Type u_2
N : Type u_1
P : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a✝ ∈ neLocus g₁ g₂
α : Type u_4
M : Type u_2
N : Type u_1
P : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
⊢ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) = neLocus g₁ g₂
ext
no goals
case a
α : Type u_4
M : Type u_2
N : Type u_1
P : Type u_3
inst✝⁵ : DecidableEq α
inst✝⁴ : DecidableEq N
inst✝³ : Zero M
inst✝² : DecidableEq P
inst✝¹ : Zero P
inst✝ : Zero N
F : M → N → P
F0 : F 0 0 = 0
f : α →₀ M
g₁ g₂ : α →₀ N
hF : ∀ (f : M), Function.Injective fun g => F f g
a✝ : α
⊢ a✝ ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a✝ ∈ neLocus g₁ g₂
simpa only [mem_neLocus] using (hF _).ne_iff