awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : γ
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 ⋯ : (a : γ) → ℝ≥0∞) a :
                ℝ≥0∞) :
          ℝ≥0∞))
⊢ 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∞))

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

Premises used: ENNReal.tsum_mul_left, ENNReal.tsum_mul_right, tsum_dite_right, Eq.symm
-- 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 : γ
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 ⋯ : (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∞))
⊢ 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∞))

Tactic:
simp only [ENNReal.tsum_eq_zero]

Premises used: ENNReal.tsum_eq_zero
-- 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 : γ
⊢ 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∞))

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

Premises used: 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 β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
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 ⋯ : (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∞)
⊢ 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∞))

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

Premises used: 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 β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
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:
ring1
-- 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 : γ
a' : α
b : β
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∞)

Tactic:
ring1
-- 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 : γ
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∞) (0 : ℝ≥0∞))

Tactic:
ring1
-- 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 : γ
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_2 : ¬Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
      ((g b ⋯ : (a : γ) → ℝ≥0∞) a : ℝ≥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∞))

Tactic:
ring1
-- 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 : γ
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∞)
neg : 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∞))

Tactic:
absurd H
-- 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 : γ
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∞)
⊢ Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simpa [h] using h_1 a'
-- 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 : γ
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_2 : Eq (α := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞))
      ((g b ⋯ : (a : γ) → ℝ≥0∞) a : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) ((p : (a : α) → ℝ≥0∞) a' : ℝ≥0∞)
      (HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((f a' h : (a : β) → ℝ≥0∞) b : ℝ≥0∞) (0 : ℝ≥0∞))

Tactic:
simp [h_2]
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
q : PMF β
f : (a : α) → a ∈ p.support → (b : β) → b ∈ q.support → PMF γ
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∞)
⊢ 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)

Tactic:
apply PMF.ext

Premises used: PMF.ext
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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 : γ
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 ⋯ 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∞))
⊢ 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∞)

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

Premises used: ENNReal.tsum_mul_left, tsum_dite_right, Eq.symm, PMF.bindOnSupport_apply
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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∞))

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

Premises used: trans, tsum_congr, ENNReal.tsum_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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 : γ
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 ⋯ 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∞)
⊢ 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∞))

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

Premises used: trans, tsum_congr, ENNReal.tsum_comm
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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∞)
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 ⋯ 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 ⋯ : (a : γ) → ℝ≥0∞) c : ℝ≥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∞)

Tactic:
split_ifs with h1 h2 h2
-- Module: Mathlib.Probability.ProbabilityMassFunction.Monad
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 : α
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:
ring