awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : γ
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 ⋯ : (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 ⋯ : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞)
have pos : ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
  (_ :
    ∀ (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),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞) * 0 =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with h _ h_1 H h_2
-- 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 : γ
a' : α
b : β
pos :
  ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ :
      ∀ (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),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞) * 0 =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (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 ⋯ : (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 ⋯ : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞)
have neg : ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
  (_ :
    ¬∀ (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),
  HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
      ((g b sorry : (a : γ) → ℝ≥0∞) a : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with h _ h_1 H h_2
-- 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 : γ
a' : α
b : β
pos :
  ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ :
      ∀ (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),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞) * 0 =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
    (_ :
      ¬∀ (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),
    HMul.hMul (β := ℝ≥0∞) (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
        ((g b ⋯ : (a : γ) → ℝ≥0∞) a : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (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 ⋯ : (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 ⋯ : (a : γ) → ℝ≥0∞) a :
              ℝ≥0∞) :
        ℝ≥0∞)
have pos₁ : ∀ (h : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞))
  (h_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∞) b :
            ℝ≥0∞) =
        0)
  (H : Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) * 0 =
    HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: split_ifs with h _ h_1 H h_2
-- 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 : γ
a' : α
b : β
h : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) (0 : ℝ≥0∞)
h_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∞) b :
          ℝ≥0∞) =
      0
H : ¬Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) * 0 =
    HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((g b ⋯ : (a : γ) → ℝ≥0∞) a : ℝ≥0∞))
have neg : Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: absurd 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 γ
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: classical
  simp only [ENNReal.tsum_eq_zero]
  refine ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => ?_)
  split_ifs with h _ h_1 H h_2
  any_goals ring1
  · absurd H
    simpa [h] using h_1 a'
  · simp [h_2]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
⊢ Eq.{u_3 + 1} (α := PMF γ) (p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ q.bindOnSupport (f a ha))
    (q.bindOnSupport fun (b : β) (hb : b ∈ q.support) ↦ p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ f a ha b hb)
have h : ∀ (x : γ),
  Eq (α := ℝ≥0∞)
    (((p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ q.bindOnSupport (f a ha) : PMF γ) : (a : γ) → ℝ≥0∞) x : ℝ≥0∞)
    (((q.bindOnSupport fun (b : β) (hb : b ∈ q.support) ↦
              p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ f a ha b hb :
            PMF γ) :
          (a : γ) → ℝ≥0∞)
        x :
      ℝ≥0∞)
Tactic: apply PMF.ext
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
⊢ Eq (α := ℝ≥0∞)
    (((p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ q.bindOnSupport (f a ha) : PMF γ) : (a : γ) → ℝ≥0∞) c : ℝ≥0∞)
    (((q.bindOnSupport fun (b : β) (hb : b ∈ q.support) ↦
              p.bindOnSupport fun (a : α) (ha : a ∈ p.support) ↦ f a ha b hb :
            PMF γ) :
          (a : γ) → ℝ≥0∞)
        c :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  (∑' (a : α) (i : β),
    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∞) ((q : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a sorry i h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞))
  (∑' (a : β) (i : α),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) a : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 sorry : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞))
Tactic: simp only [bindOnSupport_apply, ← tsum_dite_right,
    ENNReal.tsum_mul_left.symm]
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
c : γ
⊢ Eq (α := ℝ≥0∞)
    (∑' (a : α) (i : β),
      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∞) ((q : (a : β) → ℝ≥0∞) i : ℝ≥0∞)
              (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞) then 0
                else (f a ⋯ i h : (a : γ) → ℝ≥0∞) c :
                ℝ≥0∞) :
          ℝ≥0∞))
    (∑' (a : β) (i : α),
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) a : ℝ≥0∞)
        (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
          else
            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 ⋯ : (a : γ) → ℝ≥0∞) c :
                ℝ≥0∞) :
          ℝ≥0∞))
have h : ∀ (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
          HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a sorry b h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 b sorry : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞)
Tactic: refine _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => ?_)
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : 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 : α
⊢ 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∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a ⋯ b h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 b ⋯ : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞)
have pos : ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
  (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with h1 h2 h2
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : 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 : α
pos :
  ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a ⋯ b h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 b ⋯ : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞)
have neg : ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
  (h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
Tactic: split_ifs with h1 h2 h2
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : 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 : α
pos :
  ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
        (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
⊢ 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∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a ⋯ b h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 b ⋯ : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞)
have pos₁ : ∀ (h1 : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
  (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: split_ifs with h1 h2 h2
-- Lean 4 proof step from Mathlib.Probability.ProbabilityMassFunction.Monad (goal)
Goal:
α : 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 : α
pos :
  ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
neg :
  ∀ (h1 : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
        (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
pos₁ :
  ∀ (h1 : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
    (h2 : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
        (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ 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∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
            (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
              else (f a ⋯ b h : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else
          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 b ⋯ : (a : γ) → ℝ≥0∞) c :
              ℝ≥0∞) :
        ℝ≥0∞)
have neg₁ : ∀ (h1 : ¬Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞))
  (h2 : ¬Eq (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)),
  HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞) ((f a sorry b h2 : (a : γ) → ℝ≥0∞) c : ℝ≥0∞)) =
    HMul.hMul (α := ℝ≥0∞) ((q : (a : β) → ℝ≥0∞) b : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) ((f a h1 b sorry : (a : γ) → ℝ≥0∞) c : ℝ≥0∞))
Tactic: split_ifs with h1 h2 h2
-- 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 β
s : Set β
⊢ Eq (α := ℝ≥0∞) (((p.bindOnSupport f).toOuterMeasure : (a : Set β) → ℝ≥0∞) s : ℝ≥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).toOuterMeasure : (a : Set β) → ℝ≥0∞) s :
            ℝ≥0∞) :
      ℝ≥0∞)
have simp : Eq (α := ℝ≥0∞) (∑' (x : β), s.indicator (⇑(p.bindOnSupport f) : (a : β) → ℝ≥0∞) x)
  (∑' (a : α),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞)
      (if h : Eq (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a : ℝ≥0∞) (0 : ℝ≥0∞) then 0
        else ∑' (x : β), s.indicator (⇑(f a sorry) : (a : β) → ℝ≥0∞) x :
        ℝ≥0∞))
Tactic: simp only [toOuterMeasure_apply]