-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bindOnSupport_comm (p : PMF α) (q : PMF β) (f : ∀ a ∈ p.support, ∀ b ∈ q.support, PMF γ) :
    (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) =
      q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
⊢ ∀ (x : γ),
    (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) x =
      (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) x

Tactic:
rintro c

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
⊢ (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) c =
    (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
⊢ (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) =
    q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb

Tactic:
apply PMF.ext

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
⊢ ∀ (x : γ),
    (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) x =
      (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) x

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → 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 ⋯ b h) c) =
    q b * if h : q b = 0 then 0 else p a * if h : p a = 0 then 0 else (f a h b ⋯) c

Tactic:
split_ifs with h1 h2 h2 <;> ring

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
⊢ (p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) c =
    (q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb) c

Tactic:
simp only [ENNReal.coe_inj.symm, bindOnSupport_apply, ← tsum_dite_right,
  ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → 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 ⋯ i h) 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 h a ⋯) c

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → 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 ⋯ i h) 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 h a ⋯) c

Tactic:
refine _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => ?_)

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → 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 ⋯ b h) c) =
    q b * if h : q b = 0 then 0 else p a * if h : p a = 0 then 0 else (f a h b ⋯) c