-- 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_5
α : 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)
a : Set α
ha : a ∈ J
⊢ ∅ ∉ K a

Tactic:
exact hK4 a ha

Result:
no goals

Proof state:
case h.refine_4
α : 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)
a : Set α
ha : a ∈ J
⊢ ∀ t' ∈ ↑(K a), t' ⊆ a

Tactic:
rw [← sUnion_subset_iff]

Result:
case h.refine_4
α : 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)
a : Set α
ha : a ∈ J
⊢ ⋃₀ ↑(K a) ⊆ a

Proof state:
case h.refine_5
α : 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)
⊢ ∀ a ∈ J, ∅ ∉ K1 a

Tactic:
intros a ha

Result:
case h.refine_5
α : 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)
a : Set α
ha : a ∈ J
⊢ ∅ ∉ K1 a

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:
simp only [mem_coe, Set.le_eq_subset]

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