no goals
α : Type u_1
β : Type ?u.162293
γ : Type ?u.162296
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
ha : ¬a ∈ s
⊢ ↑(filter p s h) a = 0
rw [filter_apply, Set.indicator_apply_eq_zero.mpr fun ha' => absurd ha' ha, MulZeroClass.zero_mul]