case h
α : Type u_1
β : Type u_2
γ : Type ?u.108006
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
α : Type u_1
β : Type u_2
γ : Type ?u.108006
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
⊢ (bindOnSupport p fun a x => f a) = bind p f
ext b
case h
α : Type u_1
β : Type u_2
γ : Type ?u.108006
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
this : ∀ (a : α), (if ↑p a = 0 then 0 else ↑p a * ↑(f a) b) = ↑p a * ↑(f a) b
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
case h
α : Type u_1
β : Type u_2
γ : Type ?u.108006
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b :=
  fun a => ite_eq_right_iff.2 fun h => h.symm ▸ symm (MulZeroClass.zero_mul <| f a b)
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.108006
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
f : α → Pmf β
b : β
this : ∀ (a : α), (if ↑p a = 0 then 0 else ↑p a * ↑(f a) b) = ↑p a * ↑(f a) b
⊢ ↑(bindOnSupport p fun a x => f a) b = ↑(bind p f) b
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite,
  MulZeroClass.mul_zero, this]