case a
α : Type u_3
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_2
P : α → Type ?u.19293
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
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) ↔ a ∈ neLocus f g
α : Type u_3
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_2
P : α → Type ?u.19293
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
hF : ∀ (a : α), Function.Injective (F a)
⊢ neLocus (mapRange F F0 f) (mapRange F F0 g) = neLocus f g
ext a
no goals
case a
α : Type u_3
N : α → Type u_1
inst✝⁵ : DecidableEq α
M : α → Type u_2
P : α → Type ?u.19293
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
hF : ∀ (a : α), Function.Injective (F a)
a : α
⊢ a ∈ neLocus (mapRange F F0 f) (mapRange F F0 g) ↔ a ∈ neLocus f g
simpa only [mem_neLocus] using (hF a).ne_iff