-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.FinMeasAdditive (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_7
inst : AddCommMonoid β
T : Set α → β
T_empty : T ∅ = 0
h_add : FinMeasAdditive μ T
ι : Type u_8
S : ι → Set α
sι : Finset ι
hS_meas : ∀ (i : ι), MeasurableSet (S i)
hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)
revert :
  ∀ (hSp : ∀ i ∈ sι, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ sι, ∀ j ∈ sι, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
refine_1 :
  ∀
    (hSp :
      ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj :
      ∀ (i : ι),
        Membership.mem (γ := Finset ι) ∅ i →
          ∀ (j : ι), Membership.mem (γ := Finset ι) ∅ j → i ≠ j → Disjoint (S i) (S j)),
    T (⋃ (i : ι), ⋃ (_ : Membership.mem (γ := Finset ι) ∅ i), S i) = ∑ i ∈ ∅, T (S i)
refine_2 refine_2₁ refine_2₂ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = ∑ i ∈ insert a s, T (S i)
refine_2₃ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₄ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2₅ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
refine_2₆ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2₇ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₈ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
refine_2₉ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2₁₀ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₁₁ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
refine_2₁₂ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₁₃ refine_2₁₄ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)
refine_2₁₅ refine_2₁₆ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a) + T (⋃ i ∈ s, S i)
refine_2₁₇ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    T (⋃ i ∈ insert a s, S i) = T (S a ∪ ⋃ i ∈ s, S i)
refine_2₁₈ :
  ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
    (h :
      ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
        (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
    (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
    (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)),
    Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ i ∈ s, S i) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ T (⋃ i ∈ sι, S i) = ∑ i ∈ sι, T (S i)
have refine_2₁₉ : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (h :
    ∀ (hSp : ∀ i ∈ s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
      (h_disj : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → Disjoint (S i) (S j)), T (⋃ i ∈ s, S i) = ∑ i ∈ s, T (S i))
  (hps : ∀ i ∈ insert a s, Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (S i) : ℝ≥0∞) (∞ : ℝ≥0∞))
  (h_disj : ∀ i ∈ insert a s, ∀ j ∈ insert a s, i ≠ j → Disjoint (S i) (S j)), Disjoint (S a) (⋃ i ∈ s, S i)
Tactic: classical
  revert hSp h_disj
  refine Finset.induction_on sι ?_ ?_
  · simp only [Finset.notMem_empty, IsEmpty.forall_iff, iUnion_false, iUnion_empty, sum_empty,
      imp_true_iff, T_empty]
  intro a s has h hps h_disj
  rw [Finset.sum_insert has, ← h]
  swap; · exact fun i hi => hps i (Finset.mem_insert_of_mem hi)
  swap
  · exact fun i hi j hj hij =>
      h_disj i (Finset.mem_insert_of_mem hi) j (Finset.mem_insert_of_mem hj) hij
  rw [←
    h_add (S a) (⋃ i ∈ s, S i) (hS_meas a) (measurableSet_biUnion _ fun i _ => hS_meas i)
      (hps a (Finset.mem_insert_self a s))]
  · congr; convert! Finset.iSup_insert a s S
  · exact (measure_biUnion_lt_top s.finite_toSet fun i hi ↦
      (hps i <| Finset.mem_insert_of_mem hi).lt_top).ne
  · simp_rw [Set.disjoint_iUnion_right]
    intro i hi
    refine h_disj a (Finset.mem_insert_self a s) i (Finset.mem_insert_of_mem hi) fun hai ↦ ?_
    rw [← hai] at hi
    exact has hi
Cleared hypotheses: hSp, h_disj