awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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∞)
⊢ 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∞)
have neg : b ∉ s → Eq (α := ℝ≥0∞) 0 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ 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∞)
have 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∞)
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]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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
have 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∞)
Tactic: refine ENNReal.tsum_comm.trans (_root_.trans (tsum_congr fun a => ?_) p.tsum_coe)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
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∞)
have 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
Tactic: simp_rw [ENNReal.tsum_mul_left]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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
⊢ 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
have 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
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 : β), (f a h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) a
have neg : HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (1 : ℝ≥0∞) = (p : (a : α) → ℝ≥0∞) a
Tactic: rw [(f a h).tsum_coe, mul_one]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (∑' (i : β), (f a h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) =
    (p : (a : α) → ℝ≥0∞) a
have neg₁ : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
Tactic: rw [(f a h).tsum_coe, mul_one]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
⊢ (p.bindOnSupport f).support = ⋃ (a : α), ⋃ (h : a ∈ p.support), (f a h).support
have h : ∀ (x : β),
  x ∈ (p.bindOnSupport f).support ↔ Membership.mem (γ := Set β) (⋃ (a : α), ⋃ (h : a ∈ p.support), (f a h).support) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
⊢ (p.bindOnSupport fun (a : α) (x : a ∈ p.support) ↦ f a) = p.bind f
have 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∞)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (hypothesis)
Goal:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
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∞)
have 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∞)
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)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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∞) (0 : ℝ≥0∞) ↔
    ∀ (a : α) (ha : Ne (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞)),
      Eq (α := ℝ≥0∞) ((f a ha : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
have 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∞)
Tactic: simp only [bindOnSupport_apply, ENNReal.tsum_eq_zero, mul_eq_zero, or_iff_not_imp_left]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
⊢ (pure a).bindOnSupport f = f a ⋯
have refine : ∀ (b : β), Eq (α := ℝ≥0∞) (((pure a).bindOnSupport f : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a sorry : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
Tactic: refine PMF.ext fun b => ?_
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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∞)
have 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 sorry : (a : β) → ℝ≥0∞) b else 0
Tactic: refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
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
have 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 sorry : (a : β) → ℝ≥0∞) b else 0
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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
⊢ 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
have 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 sorry : (a : β) → ℝ≥0∞) b else 0
Tactic: by_cases h : a' = a
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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∞)
have 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 sorry : (a : β) → ℝ≥0∞) b else 0
Tactic: classical
  refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a (fun _ ↦ _))
  by_cases h : a' = a <;> simp [h]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 ⋯
have 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 sorry :
            PMF γ) :
          (a : γ) → ℝ≥0∞)
        a :
      ℝ≥0∞)
Tactic: refine PMF.ext fun a => ?_
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 : γ
⊢ 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∞)
have 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 sorry : (a : γ) → ℝ≥0∞) a :
                ℝ≥0∞) :
        ℝ≥0∞))
Tactic: dsimp only [bindOnSupport_apply]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 : γ
⊢ 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∞))
have simp : Eq (α := ℝ≥0∞)
  (∑' (a_1 : β) (i : α),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i 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 : α) (i : β),
    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
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (g i sorry : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞))
Tactic: simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 : γ
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : β) (i : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i 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 : α) (i : β),
      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
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
              (if h : Eq (α := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                else (g i ⋯ : (a : γ) → ℝ≥0∞) a :
                ℝ≥0∞) :
          ℝ≥0∞))
have simp : Eq (α := ℝ≥0∞)
  (∑' (a_1 : β) (i : α),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i h : (a : β) → ℝ≥0∞) a_1 :
          ℝ≥0∞) *
      if h :
          ∀ (i : α),
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
                (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                  else (f i h : (a : β) → ℝ≥0∞) a_1 :
                  ℝ≥0∞) =
              0 then
        0
      else (g a_1 sorry : (a : γ) → ℝ≥0∞) a)
  (∑' (a_1 : α) (i : β),
    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
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (g i sorry : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞))
Tactic: simp only [ENNReal.tsum_eq_zero]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
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 : γ
⊢ Eq (α := ℝ≥0∞)
    (∑' (a_1 : β) (i : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
          (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0 else (f i h : (a : β) → ℝ≥0∞) a_1 :
            ℝ≥0∞) *
        if h :
            ∀ (i : α),
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
                  (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                    else (f i h : (a : β) → ℝ≥0∞) a_1 :
                    ℝ≥0∞) =
                0 then
          0
        else (g a_1 ⋯ : (a : γ) → ℝ≥0∞) a)
    (∑' (a_1 : α) (i : β),
      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
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
              (if h : Eq (α := ℝ≥0∞) ((f a_1 h : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                else (g i ⋯ : (a : γ) → ℝ≥0∞) a :
                ℝ≥0∞) :
          ℝ≥0∞))
have refine : ∀ (a' : α) (b : β),
  (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∞) *
      if h :
          ∀ (i : α),
            HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞)
                (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                  else (f i h : (a : β) → ℝ≥0∞) b :
                  ℝ≥0∞) =
              0 then
        0
      else (g b sorry : (a : γ) → ℝ≥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
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (g b sorry : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞)
Tactic: refine ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => ?_)