-- 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:
α : 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
⊢ Disjoint ↑(hC.disjointOfDiffUnion ⋯ ⋯) ↑(K i)

Tactic:
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))

Result:
α : 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
⊢ ∀ e ∈ ↑(K i), e ≤ ⋃₀ ↑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 = ⋃₀ ↑(if True then hC.disjointOfDiffUnion ⋯ ⋯ else K s) ∪ ⋃₀ ⋃ x ∈ J, ↑(K x)

Tactic:
simp_rw [apply_ite, hK5,
← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion h1.1 h1.2, hK5]

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 ∪ ⋃₀ ⋃ x ∈ J, ↑(K x) = (if True then s \ ⋃₀ ⋃ x ∈ J, ↑(K x) else ⋃₀ ↑(K s)) ∪ ⋃₀ ⋃ x ∈ J, ↑(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 α
hi : i ∈ K1 s
j x : Set α
hx : x ∈ J
h3 : j ∈ K1 x
h4 : ¬i = j
⊢ Disjoint i j

Tactic:
obtain ki : i ⊆ s \ ⋃₀ J := hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2 _
  (hK1s ▸ hi)

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 α
hi : i ∈ K1 s
j x : Set α
hx : x ∈ J
h3 : j ∈ K1 x
h4 : ¬i = j
ki : i ⊆ s \ ⋃₀ ↑J
⊢ Disjoint i j