α : Type u_2
β : Type u_1
γ : Type ?u.45609
q : Pmf (α → β)
p : Pmf α
b : β
⊢ (∑' (a : α → β), ↑q a * ∑' (a_1 : α), if b = a a_1 then ↑p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
α : Type u_2
β : Type u_1
γ : Type ?u.45609
q : Pmf (α → β)
p : Pmf α
b : β
⊢ ↑(seq q p) b = ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
simp only [seq, mul_boole, bind_apply, pure_apply]
α : Type u_2
β : Type u_1
γ : Type ?u.45609
q : Pmf (α → β)
p : Pmf α
b : β
f : α → β
a : α
⊢ (↑q f * if b = f a then ↑p a else 0) = if b = f a then ↑q f * ↑p a else 0
α : Type u_2
β : Type u_1
γ : Type ?u.45609
q : Pmf (α → β)
p : Pmf α
b : β
⊢ (∑' (a : α → β), ↑q a * ∑' (a_1 : α), if b = a a_1 then ↑p a_1 else 0) =
    ∑' (f : α → β) (a : α), if b = f a then ↑q f * ↑p a else 0
refine' tsum_congr fun f => ENNReal.tsum_mul_left.symm.trans (tsum_congr fun a => _)
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.45609
q : Pmf (α → β)
p : Pmf α
b : β
f : α → β
a : α
⊢ (↑q f * if b = f a then ↑p a else 0) = if b = f a then ↑q f * ↑p a else 0
simpa only [MulZeroClass.mul_zero] using mul_ite (b = f a) (q f) (p a) 0