awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
⊢ Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))

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_notMem_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)
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
⊢ Function.onFun Disjoint K1 s i

Tactic:
Finset.disjoint_iff_inter_eq_empty.mpr ?_

Premises used: Iff.mpr, Finset.disjoint_iff_inter_eq_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
refine : K1 s ∩ K1 i = ∅
⊢ Function.onFun Disjoint K1 s i

Tactic:
refine Finset.disjoint_iff_inter_eq_empty.mpr ?_

Premises used: Iff.mpr, Finset.disjoint_iff_inter_eq_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
rw : hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∩ K i = ∅
⊢ K1 s ∩ K1 i = ∅

Tactic:
rw [ht1' i hi, hK1s]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
⊢ (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) ∩ (↑(K i) : Set (Set α)) = ∅

Tactic:
rw [Set.disjoint_iff_inter_eq_empty] at h7

Premises used: Set.disjoint_iff_inter_eq_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) ∩ (↑(K i) : Set (Set α)) = ∅
⊢ hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ ∩ K i = ∅

Tactic:
exact_mod_cast h7
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
⊢ Function.onFun Disjoint K1 s i

Tactic:
have h8 : Function.onFun Disjoint K1 s i := by
          refine Finset.disjoint_iff_inter_eq_empty.mpr ?_
          rw [ht1' i hi, hK1s]
          rw [Set.disjoint_iff_inter_eq_empty] at h7
          exact_mod_cast h7
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
h8 : Function.onFun Disjoint K1 s i
⊢ Function.onFun Disjoint K1 s i ∧ Function.onFun Disjoint K1 i s

Tactic:
⟨h8, Disjoint.symm h8⟩

Premises used: Disjoint.symm, And.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ (↑J : Set (Set α))
h : s ≠ i
h7 : Disjoint (↑(hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯) : Set (Set α)) (↑(K i) : Set (Set α))
h8 : Function.onFun Disjoint K1 s i
⊢ Function.onFun Disjoint K1 s i ∧ Function.onFun Disjoint K1 i s

Tactic:
exact ⟨h8, Disjoint.symm h8⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ J
h : (↑(K i) : Set (Set α)) ⊆ C
⊢ (↑(K1 i) : Set (Set α)) ⊆ C

Tactic:
rw [ht1' i hi]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ J
⊢ (↑(K i) : Set (Set α)) ⊆ C

Tactic:
hK1 i hi
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
i : Set α
hi : i ∈ J
⊢ (↑(K i) : Set (Set α)) ⊆ C

Tactic:
exact hK1 i hi
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
h : ((↑(K1 s) : Set (Set α)) ∪ ⋃ x ∈ J, (↑(K1 x) : Set (Set α))).PairwiseDisjoint id
⊢ PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id

Tactic:
simp only [iUnion_iUnion_eq_or_left]

Premises used: Set.iUnion_iUnion_eq_or_left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
⊢ ((↑(K1 s) : Set (Set α)) ∪ ⋃ x ∈ J, (↑(K1 x) : Set (Set α))).PairwiseDisjoint id

Tactic:
pairwiseDisjoint_union.mpr ⟨?_, ?_, ?_⟩

Premises used: Iff.mpr, And.intro, Set.pairwiseDisjoint_union
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J_1 : Finset (Set α)
hC : IsSetSemiring C
s : Set α
J : Finset (Set α)
hJ : s ∉ J
hind :
  ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑J : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
h1 : s ∈ C ∧ (↑J : Set (Set α)) ⊆ C
K : Set α → Finset (Set α)
hK0 : (↑J : Set (Set α)).PairwiseDisjoint K
hK1 : ∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C
hK2 : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id
hK3 : ∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j
hK4 : ∀ j ∈ J, ∅ ∉ K j
hK5 : ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))
K1 : Set α → Finset (Set α) := fun (t : Set α) ↦ if t = s then hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯ else K t
hK1s : K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯
hK1_of_ne : ∀ (t : Set α) (ht : t ≠ s), K1 t = K t
ht1' : ∀ x ∈ J, K1 x = K x
ht2 : Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))
h : (↑(K1 s) : Set (Set α)).PairwiseDisjoint id
h₁ : PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) id
h₂ :
  ∀ ⦃i : Set α⦄,
    i ∈ (↑(K1 s) : Set (Set α)) →
      ∀ ⦃j : Set α⦄,
        Membership.mem (γ := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) j → i ≠ j → Disjoint (id i) (id j)
⊢ ((↑(K1 s) : Set (Set α)) ∪ ⋃ x ∈ J, (↑(K1 x) : Set (Set α))).PairwiseDisjoint id

Tactic:
refine pairwiseDisjoint_union.mpr ⟨?_, ?_, ?_⟩

Premises used: Iff.mpr, And.intro, Set.pairwiseDisjoint_union