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