-- Mathlib/MeasureTheory/SetSemiring.lean
theorem disjointOfUnion_props (hC : IsSetSemiring C) (h1 : ↑J ⊆ C) :
    ∃ K : Set α → Finset (Set α),
      PairwiseDisjoint J K
      ∧ (∀ i ∈ J, ↑(K i) ⊆ C)
      ∧ PairwiseDisjoint (⋃ x ∈ J, (K x : Set (Set α))) id
      ∧ (∀ j ∈ J, ⋃₀ K j ⊆ j)
      ∧ (∀ j ∈ J, ∅ ∉ K j)
      ∧ ⋃₀ J = ⋃₀ (⋃ x ∈ J, (K x : Set (Set α)))

Proof state:
case cons.intro.intro.intro.intro.intro.intro
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
⊢ ∃ K,
    (↑(cons s J hJ)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, ↑(K i) ⊆ C) ∧
        (⋃ x ∈ cons s J hJ, ↑(K x)).PairwiseDisjoint id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ ↑(K j) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧ ⋃₀ ↑(cons s J hJ) = ⋃₀ ⋃ x ∈ cons s J hJ, ↑(K x)

Tactic:
have hK1_of_ne t (ht : t ≠ s) : K1 t = K t := by simp [K1, ht]

Result:
case cons.intro.intro.intro.intro.intro.intro
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
hK1_of_ne : ∀ (t : Set α), t ≠ s → K1 t = K t
⊢ ∃ K,
    (↑(cons s J hJ)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, ↑(K i) ⊆ C) ∧
        (⋃ x ∈ cons s J hJ, ↑(K x)).PairwiseDisjoint id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ ↑(K j) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧ ⋃₀ ↑(cons s J hJ) = ⋃₀ ⋃ x ∈ cons s J hJ, ↑(K x)

Proof state:
case h.refine_3.refine_3
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
hK1_of_ne : ∀ (t : Set α), t ≠ s → K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : ⋃ x ∈ J, ↑(K1 x) = ⋃ x ∈ J, ↑(K x)
⊢ ∀ ⦃i : Set α⦄, i ∈ ↑(K1 s) → ∀ ⦃j : Set α⦄, j ∈ ⋃ x ∈ J, ↑(K1 x) → i ≠ j → Disjoint (id i) (id j)

Tactic:
simp only [mem_coe, mem_iUnion, exists_prop, ne_eq, id_eq, forall_exists_index, and_imp]

Result:
case h.refine_3.refine_3
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
hK1_of_ne : ∀ (t : Set α), t ≠ s → K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : ⋃ x ∈ J, ↑(K1 x) = ⋃ x ∈ J, ↑(K x)
⊢ ∀ ⦃i : Set α⦄, i ∈ K1 s → ∀ ⦃j : Set α⦄, ∀ x ∈ J, j ∈ K1 x → ¬i = j → Disjoint i j

Proof state:
case h.refine_6
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
hK1_of_ne : ∀ (t : Set α), t ≠ s → K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : ⋃ x ∈ J, ↑(K1 x) = ⋃ x ∈ J, ↑(K x)
⊢ s ∪ ⋃₀ ↑J = ⋃₀ ⋃ x, ⋃ (_ : x = s ∨ x ∈ J), ↑(K1 x)

Tactic:
simp only [iUnion_iUnion_eq_or_left, ht2, sUnion_union, ht2, K1]

Result:
case h.refine_6
α : Type u_1
C : Set (Set α)
J✝ : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ↑J ⊆ C →
    ∃ K,
      (↑J).PairwiseDisjoint K ∧
        (∀ i ∈ J, ↑(K i) ⊆ C) ∧
          (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id ∧
            (∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j) ∧ (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
h1 : s ∈ C ∧ ↑J ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J).PairwiseDisjoint K
hK1 : ∀ i ∈ J, ↑(K i) ⊆ C
hK2 : (⋃ x ∈ J, ↑(K x)).PairwiseDisjoint id
hK3 : ∀ j ∈ J, ⋃₀ ↑(K j) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ ↑J = ⋃₀ ⋃ x ∈ J, ↑(K x)
K1 : Set α → Finset (Set α) := fun t => if t = s then hC.disjointOfDiffUnion ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion ⋯ ⋯
hK1_of_ne : ∀ (t : Set α), t ≠ s → K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : ⋃ x ∈ J, ↑(K1 x) = ⋃ x ∈ J, ↑(K x)
⊢ s ∪ ⋃₀ ↑J = ⋃₀ ↑(if True then hC.disjointOfDiffUnion ⋯ ⋯ else K s) ∪ ⋃₀ ⋃ x ∈ J, ↑(K x)