awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
refine :
  ∀ (u : Set α) (hu : u ∈ (↑I : Set (Set α))) (v : Set α)
    (hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))), u ≠ v → Disjoint (id u) (id v)
⊢ (↑I : Set (Set α)).PairwiseDisjoint id ∧
    (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id ∧
      ∀ ⦃i : Set α⦄,
        i ∈ (↑I : Set (Set α)) →
          ∀ ⦃j : Set α⦄,
            j ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) → i ≠ j → Disjoint (id i) (id j)

Tactic:
refine ⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑I : Set (Set α))
v : Set α
hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
h : u ≠ v
simp_rw : Disjoint u v
⊢ Disjoint (id u) (id v)

Tactic:
simp_rw [id]

Premises used: id
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑I : Set (Set α))
v : Set α
hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
h : u ≠ v
⊢ Disjoint u v

Tactic:
disjoint_of_subset (subset_sUnion_of_mem hu) (subset_sUnion_of_mem hv)
    (hC.disjoint_sUnion_disjointOfDiffUnion hs hI)

Premises used: MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, Set.disjoint_of_subset, Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑I : Set (Set α))
v : Set α
hv : v ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
h : u ≠ v
⊢ Disjoint u v

Tactic:
exact disjoint_of_subset (subset_sUnion_of_mem hu) (subset_sUnion_of_mem hv)
    (hC.disjoint_sUnion_disjointOfDiffUnion hs hI)

Premises used: MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiffUnion, Set.disjoint_of_subset, Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
rw : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
| s

Tactic:
rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
    hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, Set.sUnion_subset, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
conv_rhs : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s
conv_rhs₁ :
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s

Tactic:
conv_rhs => rw [← union_diff_cancel (Set.sUnion_subset hI_ss : ⋃₀ ↑I ⊆ s),
    hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, Set.sUnion_subset, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
rw : ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
| s

Tactic:
rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]

Premises used: MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
conv_rhs :
  ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) = s

Tactic:
conv_rhs => rw [← sUnion_union_sUnion_disjointOfDiffUnion_of_subset hC hs hI hI_ss]

Premises used: MeasureTheory.IsSetSemiring.sUnion_union_sUnion_disjointOfDiffUnion_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
simp_rw :
  ⋃₀ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ ⋃₀ (↑(I ∪ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))

Tactic:
simp_rw [coe_union]

Premises used: Finset.coe_union
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
hI_ss : ∀ t ∈ I, t ⊆ s
rw rw₁ :
  ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ ⋃₀ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))) =
    ⋃₀ (↑I : Set (Set α)) ∪ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))

Tactic:
rw [sUnion_union]

Premises used: Set.sUnion_union
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
h1 : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑∅ : Set (Set α)).PairwiseDisjoint K ∧
      (∀ (i : Set α), Membership.mem (γ := Finset (Set α)) ∅ i → (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α)
            (⋃ (x : Set α), ⋃ (_ : Membership.mem (γ := Finset (Set α)) ∅ x), (↑(K x) : Set (Set α))) id ∧
          (∀ (j : Set α), Membership.mem (γ := Finset (Set α)) ∅ j → ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ (j : Set α), Membership.mem (γ := Finset (Set α)) ∅ j → ∅ ∉ K j) ∧
              ⋃₀ (↑∅ : Set (Set α)) =
                ⋃₀ ⋃ (x : Set α), ⋃ (_ : Membership.mem (γ := Finset (Set α)) ∅ x), (↑(K x) : Set (Set α))

Tactic:
simp
-- 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 : (↑(cons s J hJ) : Set (Set α)) ⊆ C
⊢ s ∈ C ∧ (↑J : Set (Set α)) ⊆ C

Tactic:
rw [cons_eq_insert, coe_insert, Set.insert_subset_iff] at h1

Premises used: Set.insert_subset_iff, Finset.cons_eq_insert, Finset.coe_insert
-- 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
cons :
  ∀ (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 α))),
    ∃ (K : Set α → Finset (Set α)),
      (↑(Finset.cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ Finset.cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ Finset.cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ Finset.cons s J hJ, ∅ ∉ K j) ∧
                ⋃₀ (↑(Finset.cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(Finset.cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ Finset.cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ Finset.cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ Finset.cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(Finset.cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))

Tactic:
obtain ⟨K, hK0, ⟨hK1, hK2, hK3, hK4, hK5⟩⟩ := hind h1.2

Premises used: And.right
-- 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
⊢ K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯

Tactic:
simp [K1]
-- 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
⊢ K1 s = hC.disjointOfDiffUnion (C := C) (s := s) ⋯ ⋯

Tactic:
have hK1s : K1 s = hC.disjointOfDiffUnion h1.1 h1.2 := by simp [K1]
-- 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) ⋯ ⋯
t : Set α
ht : t ≠ s
⊢ K1 t = K t

Tactic:
simp [K1, ht]
-- 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) ⋯ ⋯
⊢ ∀ (t : Set α) (ht : t ≠ s), K1 t = K t

Tactic:
have hK1_of_ne t (ht : t ≠ s) : K1 t = K t := by simp [K1, ht]
-- 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
h :
  (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K1 ∧
    (∀ i ∈ cons s J hJ, (↑(K1 i) : Set (Set α)) ⊆ C) ∧
      PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))) id ∧
        (∀ j ∈ cons s J hJ, ⋃₀ (↑(K1 j) : Set (Set α)) ⊆ j) ∧
          (∀ j ∈ cons s J hJ, ∅ ∉ K1 j) ∧
            ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ cons s J hJ, ∅ ∉ K j) ∧
              ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K x) : Set (Set α))

Tactic:
use K1
-- 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
h :
  (insert s (↑J : Set (Set α))).PairwiseDisjoint K1 ∧
    ((↑(K1 s) : Set (Set α)) ⊆ C ∧ ∀ a ∈ J, (↑(K1 a) : Set (Set α)) ⊆ C) ∧
      PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))) id ∧
        ((∀ t' ∈ K1 s, t' ⊆ s) ∧ ∀ a ∈ J, ∀ t' ∈ K1 a, t' ⊆ a) ∧
          (∅ ∉ K1 s ∧ ∀ a ∈ J, ∅ ∉ K1 a) ∧
            s ∪ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ (x : Set α), ⋃ (_ : x = s ∨ x ∈ J), (↑(K1 x) : Set (Set α))
⊢ (↑(cons s J hJ) : Set (Set α)).PairwiseDisjoint K1 ∧
    (∀ i ∈ cons s J hJ, (↑(K1 i) : Set (Set α)) ⊆ C) ∧
      PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))) id ∧
        (∀ j ∈ cons s J hJ, ⋃₀ (↑(K1 j) : Set (Set α)) ⊆ j) ∧
          (∀ j ∈ cons s J hJ, ∅ ∉ K1 j) ∧
            ⋃₀ (↑(cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ cons s J hJ, (↑(K1 x) : Set (Set α))

Tactic:
simp only [cons_eq_insert,
      mem_coe, Finset.mem_insert, sUnion_subset_iff,
      forall_eq_or_imp, coe_insert, sUnion_insert]

Premises used: Set.sUnion_insert, Finset.mem_insert, forall_eq_or_imp, Set.sUnion_subset_iff, Finset.cons_eq_insert, Finset.coe_insert, Finset.mem_coe
-- 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
⊢ ∀ x ∈ J, K1 x = K x

Tactic:
have ht1' : ∀ x ∈ J, K1 x = K x := fun x hx ↦ hK1_of_ne _ (fun h_eq ↦ hJ (h_eq ▸ hx))
-- 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
h : ∀ (i : Set α) (j : i ∈ J), (↑(K1 i) : Set (Set α)) = (↑(K i) : Set (Set α))
⊢ Eq.{u_1 + 1} (α := Set (Set α)) (⋃ x ∈ J, (↑(K1 x) : Set (Set α))) (⋃ x ∈ J, (↑(K x) : Set (Set α)))

Tactic:
apply iUnion₂_congr

Premises used: Set.iUnion₂_congr
-- 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
x : Set α
hx : x ∈ J
⊢ (↑(K1 x) : Set (Set α)) = (↑(K x) : Set (Set α))

Tactic:
exact_mod_cast hK1_of_ne _ (ne_of_mem_of_not_mem hx hJ)

Premises used: ne_of_mem_of_not_mem