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