no goals
α : Type u_1
β : Type ?u.163622
γ : Type ?u.163625
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = 0 ↔ ¬a ∈ s ∨ ¬a ∈ support p
erw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]