-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem toOuterMeasure_bindOnSupport_apply :
    (p.bindOnSupport f).toOuterMeasure s =
      ∑' a, p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ (p.bindOnSupport f).toOuterMeasure s = ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h).toOuterMeasure s

Tactic:
simp only [toOuterMeasure_apply, Set.indicator_apply, bindOnSupport_apply]

Result:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ ∑' (x : β), s.indicator (⇑(p.bindOnSupport f)) x =
    ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), s.indicator (⇑(f a ⋯)) x

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ ∑' (x : β), s.indicator (⇑(p.bindOnSupport f)) x =
    ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), s.indicator (⇑(f a ⋯)) x

Tactic:
calc
  (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
      ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    tsum_congr fun b => by split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
  _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    ENNReal.tsum_comm
  _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
  _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
    tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
⊢ ∑' (x : β), s.indicator (⇑(p.bindOnSupport f)) x =
    ∑' (a : α), p a * if h : p a = 0 then 0 else ∑' (x : β), s.indicator (⇑(f a ⋯)) x

Tactic:
classical
calc
  (∑' b, ite (b ∈ s) (∑' a, p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0) =
      ∑' (b) (a), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    tsum_congr fun b => by split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]
  _ = ∑' (a) (b), ite (b ∈ s) (p a * dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    ENNReal.tsum_comm
  _ = ∑' a, p a * ∑' b, ite (b ∈ s) (dite (p a = 0) (fun h => 0) fun h => f a h b) 0 :=
    (tsum_congr fun a => by simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero])
  _ = ∑' a, p a * dite (p a = 0) (fun h => 0) fun h => ∑' b, ite (b ∈ s) (f a h b) 0 :=
    tsum_congr fun a => by split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
⊢ (p a * ∑' (b : β), if b ∈ s then if h : p a = 0 then 0 else (f a h) b else 0) =
    p a * if h : p a = 0 then 0 else ∑' (b : β), if b ∈ s then (f a h) b else 0

Tactic:
split_ifs with ha <;> simp only [ite_self, tsum_zero, eq_self_iff_true]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
a : α
⊢ (∑' (b : β), if b ∈ s then p a * if h : p a = 0 then 0 else (f a h) b else 0) =
    p a * ∑' (b : β), if b ∈ s then if h : p a = 0 then 0 else (f a h) b else 0

Tactic:
simp only [← ENNReal.tsum_mul_left, mul_ite, mul_zero]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
s : Set β
b : β
⊢ (if b ∈ s then ∑' (a : α), p a * if h : p a = 0 then 0 else (f a h) b else 0) =
    ∑' (a : α), if b ∈ s then p a * if h : p a = 0 then 0 else (f a h) b else 0

Tactic:
split_ifs with hbs <;> simp only [eq_self_iff_true, tsum_zero]

Result:
no goals