-- 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∞)
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∞))
neg₁ :
  ∀ (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∞))
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_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∞))
⊢ (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∞))
  (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 sorry : (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 sorry : (a : γ) → ℝ≥0∞) a : ℝ≥0∞))
Tactic: split_ifs with h _ h_1 H h_2