case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ ∀ (x : γ),
    ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) x =
      ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) x
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ (bindOnSupport p fun a ha => bindOnSupport q (f a ha)) =
    bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb
apply Pmf.ext
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) c =
    ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) c
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
⊢ ∀ (x : γ),
    ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) x =
      ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) x
rintro c
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ (∑' (a : α) (i : β),
      ↑p a *
        if h : ↑p a = 0 then 0 else ↑q i * if h : ↑q i = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) i (_ : ¬↑q i = 0)) c) =
    ∑' (a : β) (i : α),
      ↑q a * if h : ↑q a = 0 then 0 else ↑p i * if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0) a (_ : ¬↑q a = 0)) c
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ ↑(bindOnSupport p fun a ha => bindOnSupport q (f a ha)) c =
    ↑(bindOnSupport q fun b hb => bindOnSupport p fun a ha => f a ha b hb) c
simp only [ENNReal.coe_eq_coe.symm, bindOnSupport_apply, ← tsum_dite_right,
  ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
⊢ (↑p a * if h : ↑p a = 0 then 0 else ↑q b * if h : ↑q b = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * if h : ↑q b = 0 then 0 else ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
⊢ (∑' (a : α) (i : β),
      ↑p a *
        if h : ↑p a = 0 then 0 else ↑q i * if h : ↑q i = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) i (_ : ¬↑q i = 0)) c) =
    ∑' (a : β) (i : α),
      ↑q a * if h : ↑q a = 0 then 0 else ↑p i * if h : ↑p i = 0 then 0 else ↑(f i (_ : ¬↑p i = 0) a (_ : ¬↑q a = 0)) c
refine' _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => _)
no goals
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p✝ : Pmf α
f✝ : (a : α) → a ∈ support p✝ → Pmf β
p : Pmf α
q : Pmf β
f : (a : α) → a ∈ support p → (b : β) → b ∈ support q → Pmf γ
c : γ
b : β
a : α
⊢ (↑p a * if h : ↑p a = 0 then 0 else ↑q b * if h : ↑q b = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c) =
    ↑q b * if h : ↑q b = 0 then 0 else ↑p a * if h : ↑p a = 0 then 0 else ↑(f a (_ : ¬↑p a = 0) b (_ : ¬↑q b = 0)) c
split_ifs with h1 h2 h2 <;> ring