-- 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
α : 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)
⊢ (insert s ↑J).PairwiseDisjoint K1 ∧
    (↑(K1 s) ⊆ C ∧ ∀ a ∈ J, ↑(K1 a) ⊆ C) ∧
      (⋃ x, ⋃ (_ : x = s ∨ x ∈ J), ↑(K1 x)).PairwiseDisjoint id ∧
        ((∀ t' ∈ K1 s, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ K1 s ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧ s ∪ ⋃₀ ↑J = ⋃₀ ⋃ x, ⋃ (_ : x = s ∨ x ∈ J), ↑(K1 x)

Tactic:
simp only [hK1s]

Result:
case 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)
⊢ (insert s ↑J).PairwiseDisjoint K1 ∧
    (↑(hC.disjointOfDiffUnion ⋯ ⋯) ⊆ C ∧ ∀ a ∈ J, ↑(K1 a) ⊆ C) ∧
      (⋃ x, ⋃ (_ : x = s ∨ x ∈ J), ↑(K1 x)).PairwiseDisjoint id ∧
        ((∀ t' ∈ hC.disjointOfDiffUnion ⋯ ⋯, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ hC.disjointOfDiffUnion ⋯ ⋯ ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧ s ∪ ⋃₀ ↑J = ⋃₀ ⋃ x, ⋃ (_ : x = s ∨ x ∈ J), ↑(K1 x)

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
⊢ ↑(K i) ⊆ C

Tactic:
exact hK1 i hi

Result:
no goals

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
⊢ ∀ e ∈ K i, e ⊆ ⋃₀ ↑J

Tactic:
apply sUnion_subset_iff.mp

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
⊢ ⋃₀ Membership.mem (K i).val ⊆ ⋃₀ ↑J

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
ki : i ⊆ s \ ⋃₀ ↑J
⊢ Disjoint i j

Tactic:
obtain hx2 : j ⊆ x := subset_trans (subset_sUnion_of_mem (ht1' x hx ▸ h3)) (hK3 x hx)

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
hx2 : j ⊆ x
⊢ Disjoint i j