case a
α : Type u_4
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_2
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
a : α
⊢ a ∈ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) ↔ a ∈ neLocus g₁ g₂
α : Type u_4
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_2
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a f g
⊢ neLocus (zipWith F F0 f g₁) (zipWith F F0 f g₂) = neLocus g₁ g₂
ext a
no goals
case a
α : Type u_4
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_3
P : α → Type u_2
inst✝⁴ : (a : α) → Zero (N a)
inst✝³ : (a : α) → Zero (M a)
inst✝² : (a : α) → Zero (P a)
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective fun g => F a 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 a _).ne_iff