α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ b ∈ ⋃ (a : α) (h : a ∈ support p), support (f a h)
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
⊢ support (bindOnSupport p f) = ⋃ (a : α) (h : a ∈ support p), support (f a h)
refine' Set.ext fun b => _
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0) ↔
    ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ b ∈ support (bindOnSupport p f) ↔ b ∈ ⋃ (a : α) (h : a ∈ support p), support (f a h)
simp only [ENNReal.tsum_eq_zero, not_or, mem_support_iff, bindOnSupport_apply, Ne.def, not_forall,
  mul_eq_zero, Set.mem_iUnion]
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
⊢ (∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0) ↔
    ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
exact
  ⟨fun hb =>
    let ⟨a, ⟨ha, ha'⟩⟩ := hb
    ⟨a, ha, by simpa [ha] using ha'⟩,
    fun hb =>
    let ⟨a, ha, ha'⟩ := hb
    ⟨a, ⟨ha, by simpa [(mem_support_iff _ a).1 ha] using ha'⟩⟩⟩
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ x, ¬↑p x = 0 ∧ ¬(if h : ↑p x = 0 then 0 else ↑(f x (_ : ¬↑p x = 0)) b) = 0
a : α
ha : ¬↑p a = 0
ha' : ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
⊢ ¬↑(f a (_ : a ∈ support p)) b = 0
simpa [ha] using ha'
no goals
α : Type u_2
β : Type u_1
γ : Type ?u.86439
p : Pmf α
f : (a : α) → a ∈ support p → Pmf β
b : β
hb : ∃ i h, ¬↑(f i (_ : i ∈ support p)) b = 0
a : α
ha : ¬↑p a = 0
ha' : ¬↑(f a (_ : a ∈ support p)) b = 0
⊢ ¬(if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0)) b) = 0
simpa [(mem_support_iff _ a).1 ha] using ha'