-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.AddContent (goal)
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
I_1 : Finset (Set α)
G : Type u_2
inst : AddCommMonoid G
m_1 m' m : AddContent G C
hC : IsSetSemiring C
I : Finset (Set α)
hI : (↑I : Set (Set α)) ⊆ (_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C
h'I : (↑I : Set (Set α)).PairwiseDisjoint id
hh'I :
  Membership.mem (γ := Set (Set α)) ((_root_.supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
    (⋃₀ (↑I : Set (Set α)))
have :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have₁ :
  ∀
    (A :
      ∀ (s : Set α) (hs : s ∈ I),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₂ :
  ∀ (s : Set α) (hs : s ∈ I),
    ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
have₃ have₄ :
  ∀
    (A :
      ∀ (s : Set α) (hs : s ∈ I),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₅ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α))),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₆ have₇ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₈ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
      m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have₉ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
      Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
have₁₀ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))), (↑K : Set (Set α)).PairwiseDisjoint id
have₁₁ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
      Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
have₁₂ have₁₃ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))), (↑K : Set (Set α)).PairwiseDisjoint id
have₁₄ have₁₅ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
      Eq.{u_2 + 1} (α := G) (∑ s ∈ K, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
have₁₆ :
  ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
    (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
    (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
    (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
    let K := I.biUnion J;
    ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
      Eq.{u_2 + 1} (α := G) (∑ s ∈ I.biUnion J, (m : (a : Set α) → G) s) (∑ u ∈ I, m.supClosureFun (C := C) u)
⊢ m.supClosureFun (C := C) (⋃₀ (↑I : Set (Set α))) = ∑ u ∈ I, m.supClosureFun (C := C) u
have have₁₇ : ∀ (J : (s : Set α) → Finset (Set α)) (hJC : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)) ⊆ C)
  (hJdisj : ∀ (s : Set α) (hs : s ∈ I), (↑(J s) : Set (Set α)).PairwiseDisjoint id)
  (hJs : ∀ (s : Set α) (hs : s ∈ I), s = ⋃₀ (↑(J s) : Set (Set α)))
  (H : ∀ {a i : Set α} (hi : i ∈ I) (ha : a ∈ J i), a ⊆ i),
  let K := I.biUnion J;
  ∀ (this : ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑K : Set (Set α))),
    Eq.{u_2 + 1} (α := G) (∑ x ∈ I, ∑ i ∈ J x, (m : (a : Set α) → G) i) (∑ u ∈ I, m.supClosureFun (C := C) u)
Tactic: classical
    have A (s) (hs : s ∈ I) : ∃ (J : Finset (Set α)),
        ↑J ⊆ C ∧ (PairwiseDisjoint (J : Set (Set α)) id) ∧ s = ⋃₀ ↑J := by
      obtain ⟨P, PC⟩ : ∃ (P : Finpartition s), ↑P.parts ⊆ C := by
        have := hI hs
        rwa [hC.mem_supClosure_iff] at this
      refine ⟨P.parts, PC, P.disjoint, ?_⟩
      convert! P.sup_parts.symm
      simp [sUnion_eq_biUnion]
    choose! J hJC hJdisj hJs using A
    have H {a i} (hi : i ∈ I) (ha : a ∈ J i) : a ⊆ i := by
      rw [hJs i hi]
      exact subset_sUnion_of_mem ha
    let K : Finset (Set α) := Finset.biUnion I J
    have : ⋃₀ ↑I = ⋃₀ (↑K : Set (Set α)) := by grind
    rw [this, m.supClosureFun_apply hC (J := K) (by simpa [K] using hJC) _ rfl]; swap
    · simp only [K, coe_biUnion]
      refine (h'I.mono_on ?_).biUnion hJdisj
      simp
      grind
    simp only [K]
    rw [sum_biUnion_of_pairwise_eq_zero]; swap
    · intro i hi j hj hij k hk
      simp only [Finset.mem_inter] at hk
      have : Disjoint k k := by
        have : Disjoint i j := h'I hi hj hij
        exact this.mono (H hi hk.1) (H hj hk.2)
      simp only [disjoint_self, Set.bot_eq_empty] at this
      simp [this]
    apply Finset.sum_congr rfl (fun i hi ↦ Eq.symm ?_)
    exact m.supClosureFun_apply hC (hJC i hi) (hJdisj i hi) (hJs i hi)