no goals
α : Type u_1
β : Type ?u.164201
γ : Type ?u.164204
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a ≠ 0 ↔ a ∈ s ∧ a ∈ support p
rw [Ne.def, filter_apply_eq_zero_iff, not_or, Classical.not_not, Classical.not_not]