case a
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ neLocus f 0 ↔ a✝ ∈ support f
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ neLocus f 0 = support f
ext
no goals
case a
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
a✝ : α
⊢ a✝ ∈ neLocus f 0 ↔ a✝ ∈ support f
rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]