α : Type u_2
β : Type u_1
γ : Type ?u.110688
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∀ (i : α), ¬↑p i = 0 → (if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0)) b) = 0) ↔
    ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
α : Type u_2
β : Type u_1
γ : Type ?u.110688
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ ↑(bindOnSupport p f) b = 0 ↔ ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.110688
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∀ (i : α), ¬↑p i = 0 → (if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0)) b) = 0) ↔
    ∀ (a : α) (ha : ↑p a ≠ 0), ↑(f a ha) b = 0
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha),
  fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩