α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ ↑(bindOnSupport (pure a) f) b = ↑(f a (_ : a ∈ support (pure a))) b
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
⊢ bindOnSupport (pure a) f = f a (_ : a ∈ support (pure a))
refine' Pmf.ext fun b => _
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ (∑' (a_1 : α),
      (if a_1 = a then 1 else 0) *
        if h : (if a_1 = a then 1 else 0) = 0 then 0 else ↑(f a_1 (_ : ¬↑(pure a) a_1 = 0)) b) =
    ↑(f a (_ : a ∈ support (pure a))) b
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ ↑(bindOnSupport (pure a) f) b = ↑(f a (_ : a ∈ support (pure a))) b
simp only [bindOnSupport_apply, pure_apply]
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
⊢ (∑' (a_1 : α),
      (if a_1 = a then 1 else 0) *
        if h : (if a_1 = a then 1 else 0) = 0 then 0 else ↑(f a_1 (_ : ¬↑(pure a) a_1 = 0)) b) =
    ↑(f a (_ : a ∈ support (pure a))) b
refine' _root_.trans (tsum_congr fun a' => _) (tsum_ite_eq a _)
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.112939
p : Pmf α
f✝ : (a : α) → a ∈ support p → Pmf β
a : α
f : (a' : α) → a' ∈ support (pure a) → Pmf β
b : β
a' : α
⊢ ((if a' = a then 1 else 0) * if h : (if a' = a then 1 else 0) = 0 then 0 else ↑(f a' (_ : ¬↑(pure a) a' = 0)) b) =
    if a' = a then ↑(f a (_ : a ∈ support (pure a))) b else 0
by_cases h : a' = a <;> simp [h]