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
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
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
h₁ :
  Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) x)
    (⋃ i ∈ (↑(Ju (↑x : Set α) ⋯) : Set (Set α)), i)
⊢ (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) x = ⋃₀ (↑(Ju (↑x : Set α) ⋯) : Set (Set α))

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) x)
    (⋃ i ∈ (↑(Ju (↑x : Set α) ⋯) : Set (Set α)), i)

Tactic:
congr
-- 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
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
h₁ :
  Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) y)
    (⋃ i ∈ (↑(Ju (↑y : Set α) ⋯) : Set (Set α)), i)
⊢ (fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) y = ⋃₀ (↑(Ju (↑y : Set α) ⋯) : Set (Set α))

Tactic:
rw [sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion
-- 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
x : ↥J
h_2 : x ∈ (↑J.attach : Set ↥J)
y : ↥J
h_3 : y ∈ (↑J.attach : Set ↥J)
hxy : x ≠ y
hxy_disj : Disjoint (↑x : Set α) (↑y : Set α)
⊢ Eq.{u_1 + 1} (α := Set α) ((fun (i' : ↥J) ↦ (⋃ i ∈ Ju (↑i' : Set α) ⋯, i : Set α)) y)
    (⋃ i ∈ (↑(Ju (↑y : Set α) ⋯) : Set (Set α)), i)

Tactic:
congr
-- 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
⊢ ∀ i ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑i : Set α) ⋯) : Set (Set α)).PairwiseDisjoint id

Tactic:
fun u _ ↦ hJu_disj _ _

Premises used: Subtype.prop, Subtype.val
-- 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
⊢ ∀ i ∈ (↑Finset.univ : Set ↥J), (↑(Ju (↑i : Set α) ⋯) : Set (Set α)).PairwiseDisjoint id

Tactic:
exact fun u _ ↦ hJu_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.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 α)) \ t = ⋃₀ (↑J' : Set (Set α))
⊢ s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))

Tactic:
rw [coe_insert, sUnion_insert, Set.union_comm, ← Set.diff_diff, h_eq]

Premises used: Set.sUnion_insert, Set.union_comm, Set.diff_diff, 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.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 :
  Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ (↑J : Set (Set α)), i \ t)
    (⋃ i ∈ (↑(Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯) : Set (Set α)), i)
⊢ ⋃₀ (↑J : Set (Set α)) \ t = ⋃₀ (↑J' : Set (Set α))

Tactic:
simp_rw [J', sUnion_eq_biUnion, Set.iUnion_diff]

Premises used: Set.iUnion_diff, Set.sUnion_eq_biUnion
-- 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 :
  Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ J, i \ t)
    (⋃ (i : Set α), ⋃ (i_1 : Set α), ⋃ (i_2 : i_1 ∈ J), ⋃ (_ : i ∈ Ju i_1 ⋯), i)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ (↑J : Set (Set α)), i \ t)
    (⋃ i ∈ (↑(Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯) : Set (Set α)), i)

Tactic:
simp only [mem_coe, Finset.mem_biUnion, Finset.mem_univ,
      Finset.exists_coe, iUnion_exists, true_and]

Premises used: Finset.mem_univ, Set.iUnion_exists, Finset.exists_coe, Finset.mem_coe, Finset.mem_biUnion, true_and
-- 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 :
  Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ J, i \ t) (⋃ (i' : Set α), ⋃ (i : Set α), ⋃ (i_1 : i' ∈ J), ⋃ (_ : i ∈ Ju i' ⋯), i)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ J, i \ t)
    (⋃ (i : Set α), ⋃ (i_1 : Set α), ⋃ (i_2 : i_1 ∈ J), ⋃ (_ : i ∈ Ju i_1 ⋯), i)

Tactic:
rw [iUnion_comm]

Premises used: Set.iUnion_comm
-- 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
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ J, i \ t) (⋃ (i' : Set α), ⋃ (i : Set α), ⋃ (i_1 : i' ∈ J), ⋃ (_ : i ∈ Ju i' ⋯), i)

Tactic:
iUnion_congr fun i ↦ ?_

Premises used: Set.iUnion_congr
-- 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 :
  ∀ (i : Set α),
    Eq.{u_1 + 1} (α := Set α) (⋃ (_ : i ∈ J), i \ t) (⋃ (i_1 : Set α), ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ i ∈ J, i \ t) (⋃ (i' : Set α), ⋃ (i : Set α), ⋃ (i_1 : i' ∈ J), ⋃ (_ : i ∈ Ju i' ⋯), i)

Tactic:
refine iUnion_congr fun i ↦ ?_

Premises used: Set.iUnion_congr
-- 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
i : Set α
pos :
  ∀ (hi : i ∈ J),
    Eq.{u_1 + 1} (α := Set α) (⋃ (_ : i ∈ J), i \ t) (⋃ (i_1 : Set α), ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1)
neg :
  ∀ (hi : i ∉ J),
    Eq.{u_1 + 1} (α := Set α) (⋃ (_ : i ∈ J), i \ t) (⋃ (i_1 : Set α), ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1)
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (_ : i ∈ J), i \ t) (⋃ (i_1 : Set α), ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1)

Tactic:
by_cases hi : i ∈ J
-- 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
i : Set α
hi : i ∈ J
pos : i \ t = ⋃ i_1 ∈ Ju i ⋯, i_1
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (_ : i ∈ J), i \ t) (⋃ (i_1 : Set α), ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1)

Tactic:
simp only [hi, iUnion_true]

Premises used: Set.iUnion_true
-- 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
i : Set α
hi : i ∈ J
pos : Eq.{u_1 + 1} (α := Set α) (⋃ i_1 ∈ (↑(Ju i ⋯) : Set (Set α)), i_1) (⋃ i_1 ∈ Ju i ⋯, i_1)
⊢ i \ t = ⋃ i_1 ∈ Ju i ⋯, i_1

Tactic:
rw [← hJu_sUnion i (h_ss hi), sUnion_eq_biUnion]

Premises used: Set.sUnion_eq_biUnion