awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
b : β
h : b ∉ s
⊢ Eq (α := ℝ≥0∞) 0 (∑' (a : α), HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))

Tactic:
simp
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : β) (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))
    (∑' (a : α) (b : β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))

Tactic:
ENNReal.tsum_comm

Premises used: ENNReal.tsum_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α) (b : β),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))
    (∑' (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (∑' (b : β), if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞))

Tactic:
tsum_congr fun _ => ENNReal.tsum_mul_left

Premises used: ENNReal.tsum_mul_left, tsum_congr
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
pos : b ∈ s → Eq (α := ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
neg : b ∉ s → Eq (α := ℝ≥0∞) 0 0
⊢ Eq (α := ℝ≥0∞) (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)
    (if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞)

Tactic:
split_ifs
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h : b ∈ s
⊢ Eq (α := ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
b : β
h : b ∉ s
⊢ Eq (α := ℝ≥0∞) 0 0

Tactic:
rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
a : α
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (b : β), if b ∈ s then (f a : (a : β) → ℝ≥0∞) b else 0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (((f a).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
simp only [toOuterMeasure_apply, Set.indicator_apply]

Premises used: Set.indicator_apply, PMF.toOuterMeasure_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
s₁ :
  Eq (α := ℝ≥0∞) (((p.bind f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (b : β),
        if b ∈ s then
          ∑' (a : α),
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
        else 0 :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.bind f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (((f a).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
calc
    (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
      simp [toOuterMeasure_apply, Set.indicator_apply]
    _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
    _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 := ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
      (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
    _ = ∑' a, p a * (f a).toOuterMeasure s :=
      tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

Premises used: ENNReal.tsum_mul_left, HMul.hMul, tsum_congr, PMF.bind, PMF.toOuterMeasure, congr_arg, ENNReal.tsum_comm, DFunLike.coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
s₁ :
  Eq (α := ℝ≥0∞) (((p.bind f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (b : β),
        if b ∈ s then
          ∑' (a : α),
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
        else 0 :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.bind f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (((f a).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
classical
  calc
    (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
      simp [toOuterMeasure_apply, Set.indicator_apply]
    _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
    _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 := ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
      (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
    _ = ∑' a, p a * (f a).toOuterMeasure s :=
      tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

Premises used: ENNReal.tsum_mul_left, HMul.hMul, tsum_congr, PMF.bind, PMF.toOuterMeasure, congr_arg, ENNReal.tsum_comm, DFunLike.coe
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
inst : MeasurableSpace β
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((p.bind f).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          ((((f a).toMeasure : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
(toMeasure_apply_eq_toOuterMeasure_apply (p.bind f) hs).trans
    ((toOuterMeasure_bind_apply p f s).trans
      (tsum_congr fun a =>
        congr_arg (fun x => p a * x) (toMeasure_apply_eq_toOuterMeasure_apply (f a) hs).symm))

Premises used: HMul.hMul, tsum_congr, PMF.bind, PMF.toMeasure_apply_eq_toOuterMeasure_apply, congr_arg, Eq.symm, DFunLike.coe, PMF.toOuterMeasure_bind_apply, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : β) (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))
    1

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

Premises used: PMF.tsum_coe, trans, tsum_congr, ENNReal.tsum_comm, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
refine :
  ∀ (a : α),
    Eq (α := ℝ≥0∞)
      (∑' (a_1 : β),
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) a_1 :
              ℝ≥0∞) :
        ℝ≥0∞)
      ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    (∑' (b : β) (a : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
          ℝ≥0∞))
    1

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

Premises used: PMF.tsum_coe, trans, tsum_congr, ENNReal.tsum_comm, Eq.trans
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
simp_rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (i : β),
          if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) i :
        ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) a
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : β),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) a_1 :
            ℝ≥0∞) :
      ℝ≥0∞)
    ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)

Tactic:
simp_rw [ENNReal.tsum_mul_left]

Premises used: ENNReal.tsum_mul_left
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
pos :
  ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (i : β), 0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) a
neg :
  ∀ (h : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (i : β), (f a h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) =
      (p : (a : α) → ℝ≥0∞) a
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (∑' (i : β),
          if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) i :
        ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) a

Tactic:
split_ifs with h
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (i : β), 0 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) a

Tactic:
simp only [h, zero_mul]

Premises used: MulZeroClass.zero_mul
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
h : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)
neg : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) a
neg₁ neg₂ : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (i : β), (f a h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) a

Tactic:
rw [(f a h).tsum_coe, mul_one]

Premises used: PMF.tsum_coe, mul_one
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ Eq (α := ℝ≥0∞) ((p.bindOnSupport f : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    (∑' (a : α),
        HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) b :
            ℝ≥0∞) :
      ℝ≥0∞)

Tactic:
rfl

Premises used: tsum, rfl
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
h :
  ∀ (x : β),
    x ∈ (p.bindOnSupport f).support ↔ Membership.mem (γ := Set β) (⋃ (a : α), ⋃ (h : a ∈ p.support), (f a h).support) x
⊢ (p.bindOnSupport f).support = ⋃ (a : α), ⋃ (h : a ∈ p.support), (f a h).support

Tactic:
ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
x : β
⊢ x ∈ (p.bindOnSupport f).support ↔ Membership.mem (γ := Set β) (⋃ (a : α), ⋃ (h : a ∈ p.support), (f a h).support) x

Tactic:
simp only [mem_support_iff, bindOnSupport_apply, ne_eq, ENNReal.tsum_eq_zero,
    dite_eq_left_iff, mul_eq_zero, not_forall, not_or, and_exists_self,
    Set.mem_iUnion]

Premises used: Set.mem_iUnion, and_exists_self, mul_eq_zero, ne_eq, not_or, PMF.mem_support_iff, dite_eq_left_iff, Classical.not_forall, PMF.bindOnSupport_apply, ENNReal.tsum_eq_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ b ∈ (p.bindOnSupport f).support ↔ ∃ (a : α) (h : a ∈ p.support), b ∈ (f a h).support

Tactic:
simp only [support_bindOnSupport, Set.mem_iUnion]

Premises used: Set.mem_iUnion, PMF.support_bindOnSupport
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
h :
  ∀ (b : β),
    Eq (α := ℝ≥0∞) (((p.bindOnSupport fun (a : α) (x : a ∈ p.support) ↦ f a : PMF β) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      ((p.bind f : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
⊢ (p.bindOnSupport fun (a : α) (x : a ∈ p.support) ↦ f a) = p.bind f

Tactic:
ext b
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ ∀ (a : α),
    (if Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
      else HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b :=
    fun a => ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
this :
  ∀ (a : α),
    (if Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
      else HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((p.bindOnSupport fun (a : α) (x : a ∈ p.support) ↦ f a : PMF β) : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
    ((p.bind f : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite,
    mul_zero, this]

Premises used: mul_ite, MulZeroClass.mul_zero, dite_eq_ite, PMF.bind_apply, PMF.bindOnSupport_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
simp :
  (∀ (i : α),
      ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i h : (a : β) → ℝ≥0∞) b) 0) ↔
    ∀ (a : α) (ha : Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((f a ha : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((p.bindOnSupport f : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) ↔
    ∀ (a : α) (ha : Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((f a ha : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]

Premises used: mul_eq_zero, Classical.or_iff_not_imp_left, PMF.bindOnSupport_apply, ENNReal.tsum_eq_zero
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∀ (i : α),
      ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i h : (a : β) → ℝ≥0∞) b) 0) ↔
    ∀ (a : α) (ha : Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((f a ha : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha),
    fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩

Premises used: Trans.trans, dif_neg, Iff.intro
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
b : β
⊢ (∀ (i : α),
      ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) →
        Eq (α := ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i h : (a : β) → ℝ≥0∞) b) 0) ↔
    ∀ (a : α) (ha : Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((f a ha : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact ⟨fun h a ha => Trans.trans (dif_neg ha).symm (h a ha),
    fun h a ha => Trans.trans (dif_neg ha) (h a ha)⟩
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
⊢ (pure a).bindOnSupport f = f a ⋯

Tactic:
PMF.ext fun b => ?_

Premises used: PMF.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
refine :
  ∀ (b : β), Eq (α := ℝ≥0∞) (((pure a).bindOnSupport f : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
⊢ (pure a).bindOnSupport f = f a ⋯

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

Premises used: PMF.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : α),
        HMul.hMul (α := ℝ≥0∞) (if a_1 = a then 1 else 0)
          (if h : Eq (α := ℝ≥0∞) (if a_1 = a then 1 else 0) 0 then 0 else (f a_1 h : (a : β) → ℝ≥0∞) b) :
      ℝ≥0∞)
    ((f a ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
_root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))

Premises used: trans, tsum_congr, tsum_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
refine :
  ∀ (a' : α),
    HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
        (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
      if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : α),
        HMul.hMul (α := ℝ≥0∞) (if a_1 = a then 1 else 0)
          (if h : Eq (α := ℝ≥0∞) (if a_1 = a then 1 else 0) 0 then 0 else (f a_1 h : (a : β) → ℝ≥0∞) b) :
      ℝ≥0∞)
    ((f a ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))

Premises used: trans, tsum_congr, tsum_ite_eq, SummationFilter.unconditional
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
pos :
  ∀ (h : a' = a),
    HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
        (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
      if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0
neg :
  ∀ (h : ¬a' = a),
    HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
        (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
      if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0
⊢ HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
      (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
    if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0

Tactic:
by_cases h : a' = a
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : a' = a
⊢ HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
      (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
    if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0

Tactic:
simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
a' : α
h : ¬a' = a
⊢ HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
      (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
    if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0

Tactic:
simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
refine :
  ∀ (a' : α),
    HMul.hMul (α := ℝ≥0∞) (if a' = a then 1 else 0)
        (if h : Eq (α := ℝ≥0∞) (if a' = a then 1 else 0) 0 then 0 else (f a' h : (a : β) → ℝ≥0∞) b) =
      if a' = a then (f a ⋯ : (a : β) → ℝ≥0∞) b else 0
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : α),
        HMul.hMul (α := ℝ≥0∞) (if a_1 = a then 1 else 0)
          (if h : Eq (α := ℝ≥0∞) (if a_1 = a then 1 else 0) 0 then 0 else (f a_1 h : (a : β) → ℝ≥0∞) b) :
      ℝ≥0∞)
    ((f a ⋯ : (a : β) → ℝ≥0∞) b : ℝ≥0∞)

Tactic:
classical
  refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))
  by_cases h : a' = a <;> simp [h]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
p : PMF α
⊢ (p.bindOnSupport fun (a : α) (x : a ∈ p.support) ↦ pure a) = p

Tactic:
simp only [PMF.bind_pure, PMF.bindOnSupport_eq_bind]

Premises used: PMF.bindOnSupport_eq_bind, PMF.bind_pure
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : 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 : a ∈ p.support) ↦
      (f a ha).bindOnSupport fun (b : β) (hb : b ∈ (f a ha).support) ↦ g b ⋯

Tactic:
PMF.ext fun a => ?_

Premises used: PMF.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : 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 γ
refine :
  ∀ (a : γ),
    Eq (α := ℝ≥0∞) (((p.bindOnSupport f).bindOnSupport g : (a : γ) → ℝ≥0∞) a : ℝ≥0∞)
      (((p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦
                (f a ha).bindOnSupport fun (b : β) (hb : b ∈ (f a ha).support) ↦ g b ⋯ :
              PMF γ) :
            (a : γ) → ℝ≥0∞)
          a :
        ℝ≥0∞)
⊢ (p.bindOnSupport f).bindOnSupport g =
    p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦
      (f a ha).bindOnSupport fun (b : β) (hb : b ∈ (f a ha).support) ↦ g b ⋯

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

Premises used: PMF.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : 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 : γ
dsimp :
  Eq (α := ℝ≥0∞)
    (∑' (a_1 : β),
      HMul.hMul (α := ℝ≥0∞)
        (∑' (a : α),
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f a h : (a : β) → ℝ≥0∞) a_1 :
              ℝ≥0∞))
        (if h :
            Eq (α := ℝ≥0∞)
              (∑' (a : α),
                HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
                  (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                    else (f a h : (a : β) → ℝ≥0∞) a_1 :
                    ℝ≥0∞))
              0 then
          0
        else (g a_1 h : (a : γ) → ℝ≥0∞) a))
    (∑' (a_1 : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a_1 : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a_1 : ℝ≥0∞) (0 : ℝ≥0∞) then 0
          else
            ∑' (a_2 : β),
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) a_2 : ℝ≥0∞)
                (if h : Eq (α := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) a_2 : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                  else (g a_2 ⋯ : (a : γ) → ℝ≥0∞) a :
                  ℝ≥0∞) :
          ℝ≥0∞))
⊢ Eq (α := ℝ≥0∞) (((p.bindOnSupport f).bindOnSupport g : (a : γ) → ℝ≥0∞) a : ℝ≥0∞)
    (((p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦
              (f a ha).bindOnSupport fun (b : β) (hb : b ∈ (f a ha).support) ↦ g b ⋯ :
            PMF γ) :
          (a : γ) → ℝ≥0∞)
        a :
      ℝ≥0∞)

Tactic:
dsimp only [bindOnSupport_apply]

Premises used: PMF.bindOnSupport_apply