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 : (↑∅ : Set (Set α)) ⊆ C
empty :
  ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑∅ : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
simp only [coe_empty, sUnion_empty, diff_empty]

Premises used: Finset.coe_empty, Set.diff_empty, Set.sUnion_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑∅ : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩

Premises used: Iff.mpr, Finset.singleton_subset_set_iff, And.intro, Exists.intro, Singleton.singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑∅ : Set (Set α)) ⊆ C
empty : (↑{s} : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑{s} : Set (Set α))
⊢ ∃ (J : Finset (Set α)), (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑J : Set (Set α))

Tactic:
refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑∅ : Set (Set α)) ⊆ C
⊢ (↑{s} : Set (Set α)).PairwiseDisjoint id ∧ s = ⋃₀ (↑{s} : Set (Set α))

Tactic:
simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton,
      and_self_iff]

Premises used: Finset.coe_singleton, Set.sUnion_singleton, and_self_iff, Set.pairwiseDisjoint_singleton
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : (↑(insert t I') : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
?_
-- 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
insert :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : (↑(Insert.insert t I') : Set (Set α)) ⊆ C),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧
              s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
induction I using Finset.induction with
  | empty =>
    simp only [coe_empty, sUnion_empty, diff_empty]
    refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
    simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton,
      and_self_iff]
  | insert t I' _ h => ?_

Premises used: Finset.coe_singleton, Finset.coe_empty, Set.sUnion_singleton, Insert.insert, Set.diff_empty, and_self_iff, Set.pairwiseDisjoint_singleton, Set.sUnion_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : (↑(insert t I') : Set (Set α)) ⊆ C
⊢ insert t (↑I' : Set (Set α)) ⊆ C

Tactic:
rw [coe_insert] at hI

Premises used: Finset.coe_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
⊢ t ∈ C

Tactic:
have ht : t ∈ C := hI (Set.mem_insert _ _)
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
insert :
  ∀ (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C) (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id)
    (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
obtain ⟨J, h_ss, h_dis, h_eq⟩ := h ((Set.subset_insert _ _).trans hI)

Premises used: HasSubset.Subset.trans, Set.subset_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
u : Set α
hu : u ∈ C
x : Set α
hx : x ∈ (↑(Ju u hu) : Set (Set α))
⊢ x ∈ C

Tactic:
hC.subset_disjointOfDiff hu ht hx

Premises used: MeasureTheory.IsSetSemiring.subset_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
u : Set α
hu : u ∈ C
x : Set α
hx : x ∈ (↑(Ju u hu) : Set (Set α))
⊢ x ∈ C

Tactic:
exact hC.subset_disjointOfDiff hu ht hx

Premises used: MeasureTheory.IsSetSemiring.subset_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
⊢ ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C

Tactic:
have hJu_subset : ∀ (u) (hu : u ∈ C), ↑(Ju u hu) ⊆ C := by
    intro u hu x hx
    exact hC.subset_disjointOfDiff hu ht hx
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
⊢ ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id

Tactic:
have hJu_disj : ∀ (u) (hu : u ∈ C), (Ju u hu : Set (Set α)).PairwiseDisjoint id := fun u hu ↦
    hC.pairwiseDisjoint_disjointOfDiff hu ht
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
⊢ ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t

Tactic:
have hJu_sUnion : ∀ (u) (hu : u ∈ C), ⋃₀ (Ju u hu : Set (Set α)) = u \ t :=
    fun u hu ↦ hC.sUnion_disjointOfDiff hu ht
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
rw : Disjoint (u \ t) (v \ t)
⊢ Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))

Tactic:
rw [hJu_sUnion, hJu_sUnion]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
⊢ Disjoint (u \ t) (v \ t)

Tactic:
disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj

Premises used: Set.diff_subset, Set.disjoint_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
⊢ Disjoint (u \ t) (v \ t)

Tactic:
exact disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj

Premises used: Set.diff_subset, Set.disjoint_of_subset
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
⊢ ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))

Tactic:
have hJu_disj' : ∀ (u) (hu : u ∈ C) (v) (hv : v ∈ C) (_h_dis : Disjoint u v),
      Disjoint (⋃₀ (Ju u hu : Set (Set α))) (⋃₀ ↑(Ju v hv)) := by
    intro u hu v hv huv_disj
    rw [hJu_sUnion, hJu_sUnion]
    exact disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
u : Set α
simp : ∀ (x : Set α) (h : x ∈ J), u ∈ Ju x ⋯ → u ∈ C
⊢ u ∈ (↑J' : Set (Set α)) → u ∈ C

Tactic:
simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true,
      mem_iUnion, Finset.exists_coe, exists₂_imp]

Premises used: Finset.coe_biUnion, Set.mem_iUnion, Finset.mem_attach, Finset.univ_eq_attach, Set.iUnion_true, exists₂_imp, Finset.exists_coe, Finset.mem_coe
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
u v : Set α
hv : v ∈ J
huvt : u ∈ Ju v ⋯
⊢ u ∈ C

Tactic:
hJu_subset v (h_ss hv) huvt
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
u v : Set α
hv : v ∈ J
huvt : u ∈ Ju v ⋯
⊢ u ∈ C

Tactic:
exact hJu_subset v (h_ss hv) huvt
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
⊢ (↑J' : Set (Set α)) ⊆ C

Tactic:
have hJ'_subset : ↑J' ⊆ C := by
    intro u
    simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true,
      mem_iUnion, Finset.exists_coe, exists₂_imp]
    intro v hv huvt
    exact hJu_subset v (h_ss hv) huvt
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
⟨J', hJ'_subset, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
h_1 : t ∉ I'
h :
  ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : (↑J : Set (Set α)) ⊆ C
h_dis : (↑J : Set (Set α)).PairwiseDisjoint id
h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
Ju : (u : Set α) → u ∈ C → Finset (Set α) :=
  fun (u : Set α) (hu : u ∈ C) ↦ hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t
hJu_disj' :
  ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
    Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))
J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
insert : (↑J' : Set (Set α)).PairwiseDisjoint id
insert₁ : s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧
      (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
refine ⟨J', hJ'_subset, ?_, ?_⟩