-- 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 h.refine_2
α : 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 α
hi : i ∈ J
⊢ ↑(K1 i) ⊆ C

Tactic:
rw [ht1' i hi]

Result:
case h.refine_2
α : 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 α
hi : i ∈ J
⊢ ↑(K i) ⊆ C

Proof state:
case h.refine_3.refine_1
α : 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)
⊢ (↑(K1 s)).PairwiseDisjoint id

Tactic:
rw [hK1s]

Result:
case h.refine_3.refine_1
α : 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)
⊢ (↑(hC.disjointOfDiffUnion ⋯ ⋯)).PairwiseDisjoint id

Proof state:
case h.refine_1.h
α : 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 α
hi : i ∈ ↑J
a✝ : s ≠ i
⊢ Function.onFun Disjoint K1 s i ∧ Function.onFun Disjoint K1 i s

Tactic:
have h7 : Disjoint ↑(hC.disjointOfDiffUnion h1.1 h1.2) (K i : Set (Set α)) := by
  refine disjoint_of_sSup_disjoint_of_le_of_le
    (hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2) ?_
    (@disjoint_sdiff_left _ (⋃₀ J) s) (Or.inl
      (hC.empty_nmem_disjointOfDiffUnion h1.1 h1.2))
  simp only [mem_coe, Set.le_eq_subset]
  apply sUnion_subset_iff.mp
  exact (hK3 i hi).trans (subset_sUnion_of_mem hi)

Result:
case h.refine_1.h
α : 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 α
hi : i ∈ ↑J
a✝ : s ≠ i
h7 : Disjoint ↑(hC.disjointOfDiffUnion ⋯ ⋯) ↑(K i)
⊢ Function.onFun Disjoint K1 s i ∧ Function.onFun Disjoint K1 i s