-- 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 : γ
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∞))
have simp₁ : ∀ (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: 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]