-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : MeasurableSet s
t' : ℕ → Set α
ht' : s ⊆ iUnion t'
t : Set α :=
  ⋃ (n : ℕ),
    ⋃ (_ :
      Membership.mem (γ := Set ℕ)
        {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
        n),
      t' n
ht :
  t =
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₁ :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
hcap :
  tᶜ ∩ s ⊆
    ⋃ (n : ℕ),
      ⋃ (_ :
        Membership.mem (γ := Set ℕ)
          {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}
          n),
        t' n
hle₂ :
  LE.le (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (tᶜ ∩ s) : ℝ≥0∞)
    (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)) :
      ℝ≥0∞)
heq :
  Eq (α := Set ℕ)
    ({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
      {k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)})
    univ
⊢ HAdd.hAdd (α := ℝ≥0∞)
      (∑' (n :
        (↑{k : ℕ |
              LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
      (∑' (n :
        (↑{k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
          Type)),
        (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
    ∑' (x :
      (↑({k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} ∪
            {k : ℕ |
              LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)}) :
        Type)),
      min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ)))
have refine_2 : HAdd.hAdd (α := ℝ≥0∞)
    (∑' (n :
      (↑{k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      (μ : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ)))
    (∑' (n :
      (↑{k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      (ν : (a : Set α) → ℝ≥0∞) (t' (↑n : ℕ))) ≤
  HAdd.hAdd (α := ℝ≥0∞)
    (∑' (x :
      (↑{k : ℕ | LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))))
    (∑' (x :
      (↑{k : ℕ | LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t' k) : ℝ≥0∞)} :
        Type)),
      min ((μ : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))) ((ν : (a : Set α) → ℝ≥0∞) (t' (↑x : ℕ))))
Tactic: rw [ENNReal.summable.tsum_union_disjoint (f := fun n ↦ μ (t' n) ⊓ ν (t' n)) ?_ ENNReal.summable]