no goals
α : Type u_1
β : Type ?u.161365
γ : Type ?u.161368
p : Pmf α
s : Set α
h : ∃ a, a ∈ s ∧ a ∈ support p
a : α
⊢ ↑(filter p s h) a = Set.indicator s (↑p) a * (∑' (a' : α), Set.indicator s (↑p) a')⁻¹
rw [filter, normalize_apply]