-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem bindOnSupport_bindOnSupport (p : PMF α) (f : ∀ a ∈ p.support, PMF β)
    (g : ∀ b ∈ (p.bindOnSupport f).support, PMF γ) :
    (p.bindOnSupport f).bindOnSupport g =
      p.bindOnSupport fun a ha =>
        (f a ha).bindOnSupport fun b hb =>
          g b ((mem_support_bindOnSupport_iff f b).mpr ⟨a, ha, hb⟩)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) = 0 then 0 else (g a_1 ⋯) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a

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

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
⊢ ((p a' * if h : p a' = 0 then 0 else (f a' h) b) *
      if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0 then 0 else (g b ⋯) a) =
    p a' * if h : p a' = 0 then 0 else (f a' h) b * if h : (f a' h) b = 0 then 0 else (g b ⋯) a

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
_ : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
have := h_1 a'

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
_ : ¬(f a' h) b = 0
this : (p a' * if h : p a' = 0 then 0 else (f a' h) b) = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

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

Tactic:
dsimp only [bindOnSupport_apply]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β),
      (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α),
      p a_1 *
        if h : p a_1 = 0 then 0 else ∑' (a_2 : β), (f a_1 h) a_2 * if h : (f a_1 h) a_2 = 0 then 0 else (g a_2 ⋯) a

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
_ : ¬(f a' h) b = 0
this : (p a' * if h : p a' = 0 then 0 else (f a' h) b) = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
simp? [h] at this says simp only [h, ↓reduceDIte, mul_eq_zero, false_or] at this

Result:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
_ : ¬(f a' h) b = 0
this : (f a' ⋯) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
ring1

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β),
      (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α),
      p a_1 *
        if h : p a_1 = 0 then 0 else ∑' (a_2 : β), (f a_1 h) a_2 * if h : (f a_1 h) a_2 = 0 then 0 else (g a_2 ⋯) a

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

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a

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

Tactic:
refine PMF.ext fun a => ?_

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

Proof state:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
_ : ¬(f a' h) b = 0
this : (f a' ⋯) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : (∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) a_1) = 0 then 0 else (g a_1 h) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a

Tactic:
simp only [ENNReal.tsum_eq_zero, dite_eq_left_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
⊢ (∑' (a_1 : β) (i : α),
      (p i * if h : p i = 0 then 0 else (f i h) a_1) *
        if h : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) a_1) = 0 then 0 else (g a_1 ⋯) a) =
    ∑' (a_1 : α) (i : β),
      p a_1 * if h : p a_1 = 0 then 0 else (f a_1 h) i * if h : (f a_1 h) i = 0 then 0 else (g i ⋯) a