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

Tactic:
simp only [mem_coe]

Premises used: 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 α) ⋯
hJ'_subset : (↑J' : Set (Set α)) ⊆ C
i : Set α
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)

Tactic:
simp only [hi, iUnion_of_empty, iUnion_empty]

Premises used: Set.iUnion_of_empty, Set.iUnion_empty
-- 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
⊢ ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) hs hI

Tactic:
simp only [disjointOfDiffUnion, mem_sdiff, Finset.mem_singleton,
    not_true, and_false, not_false_iff]

Premises used: Finset.mem_singleton, Finset.mem_sdiff, not_true, and_false, not_false_iff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
⊢ ∅ ∉ hC.disjointOfDiffUnion (C := C) (s := s) hs hI

Tactic:
classical
  simp only [disjointOfDiffUnion, mem_sdiff, Finset.mem_singleton,
    not_true, and_false, not_false_iff]

Premises used: Finset.mem_singleton, Finset.mem_sdiff, not_true, and_false, not_false_iff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
simp :
  (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C
⊢ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]

Premises used: Finset.coe_singleton, Finset.coe_sdiff, Set.diff_singleton_subset_iff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
⊢ (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C

Tactic:
(hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, HasSubset.Subset.trans, And.left, 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
hI : (↑I : Set (Set α)) ⊆ C
⊢ (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C

Tactic:
exact (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, HasSubset.Subset.trans, And.left, 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
hI : (↑I : Set (Set α)) ⊆ C
simp :
  (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C
⊢ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ C

Tactic:
classical
  simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
  exact (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, Set.diff_singleton_subset_iff, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, HasSubset.Subset.trans, And.left, MeasureTheory.IsSetSemiring.disjointOfDiffUnion, 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
hI : (↑I : Set (Set α)) ⊆ C
simp :
  ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id
⊢ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
⊢ ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id

Tactic:
Set.PairwiseDisjoint.subset
    (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Set.PairwiseDisjoint.subset, And.right, And.left
-- 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
⊢ ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id

Tactic:
exact Set.PairwiseDisjoint.subset
    (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Set.PairwiseDisjoint.subset, And.right, And.left
-- 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
simp :
  ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id
⊢ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)).PairwiseDisjoint id

Tactic:
classical
  simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]
  exact Set.PairwiseDisjoint.subset
    (hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.1 diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, Set.PairwiseDisjoint.subset, And.right, And.left, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
rw :
  ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))

Tactic:
rw [(hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.2]

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, And.right
-- 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
simp :
  ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀
      ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅})
⊢ ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))

Tactic:
simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
rw rw₁ :
  ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀
      ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅})

Tactic:
rw [sUnion_diff_singleton_empty]

Premises used: Set.sUnion_diff_singleton_empty
-- 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
rw rw₁ rw₂ :
  ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
rw₃ :
  ⋃₀
      (↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀
      ((↑(⋯.choose (p := fun (J : Finset (Set α)) ↦
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))) :
          Set (Set α)) \
        {∅})
⊢ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))

Tactic:
classical
  rw [(hC.exists_disjoint_finset_diff_eq hs hI).choose_spec.2.2]
  simp only [disjointOfDiffUnion, coe_sdiff, coe_singleton]
  rw [sUnion_diff_singleton_empty]

Premises used: Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq, And.right, Set.sUnion_diff_singleton_empty, MeasureTheory.IsSetSemiring.disjointOfDiffUnion
-- 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
rw : s \ ⋃₀ (↑I : Set (Set α)) ⊆ s
⊢ ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ s

Tactic:
rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion
-- 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
⊢ s \ ⋃₀ (↑I : Set (Set α)) ⊆ s

Tactic:
diff_subset

Premises used: Set.diff_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
⊢ s \ ⋃₀ (↑I : Set (Set α)) ⊆ s

Tactic:
exact diff_subset

Premises used: Set.diff_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
t : Set α
ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
revert :
  ∀ (t : Set α) (ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))),
    t ⊆ s \ ⋃₀ (↑I : Set (Set α))
⊢ t ⊆ s \ ⋃₀ (↑I : Set (Set α))

Tactic:
revert t ht
-- 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
rw : ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆ s \ ⋃₀ (↑I : Set (Set α))
rw₁ rw₂ :
  ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)) ⊆
    ⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ ∀ (t : Set α) (ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))),
    t ⊆ s \ ⋃₀ (↑I : Set (Set α))

Tactic:
rw [← sUnion_subset_iff, hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion hs hI]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion, Set.sUnion_subset_iff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
apply : s \ ⋃₀ (↑I : Set (Set α)) ≤ s
⊢ t ⊆ s

Tactic:
apply le_trans <| hC.subset_of_diffUnion_disjointOfDiffUnion hs hI t ht

Premises used: MeasureTheory.IsSetSemiring.subset_of_diffUnion_disjointOfDiffUnion, le_trans
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ s \ ⋃₀ (↑I : Set (Set α)) ≤ s

Tactic:
sdiff_le (a := s) (b := ⋃₀ I)

Premises used: sdiff_le
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
t : Set α
ht : t ∈ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))
⊢ s \ ⋃₀ (↑I : Set (Set α)) ≤ s

Tactic:
exact sdiff_le (a := s) (b := ⋃₀ I)

Premises used: sdiff_le
-- 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
rw : Disjoint (⋃₀ (↑I : Set (Set α))) (s \ ⋃₀ (↑I : Set (Set α)))
⊢ Disjoint (⋃₀ (↑I : Set (Set α))) (⋃₀ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α)))

Tactic:
rw [← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion]

Premises used: MeasureTheory.IsSetSemiring.diff_sUnion_eq_sUnion_disjointOfDiffUnion
-- 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
⊢ Disjoint (⋃₀ (↑I : Set (Set α))) (s \ ⋃₀ (↑I : Set (Set α)))

Tactic:
Set.disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- 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
⊢ Disjoint (⋃₀ (↑I : Set (Set α))) (s \ ⋃₀ (↑I : Set (Set α)))

Tactic:
exact Set.disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- 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
by_contra : ∀ (h : ¬Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)), False
⊢ Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)

Tactic:
by_contra h
-- 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 : ¬Disjoint I (hC.disjointOfDiffUnion (C := C) (s := s) hs hI)
⊢ ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI

Tactic:
rw [Finset.not_disjoint_iff] at h

Premises used: Finset.not_disjoint_iff
-- 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 : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
obtain :
  ∀ (u : Set α) (huI : u ∈ I) (hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI), False
⊢ False

Tactic:
obtain ⟨u, huI, hu_disjointOfDiffUnion⟩ := h
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
⊢ u ≤ ⊥

Tactic:
have h_disj : u ≤ ⊥ :=
    hC.disjoint_sUnion_disjointOfDiffUnion hs hI (subset_sUnion_of_mem huI)
    (subset_sUnion_of_mem hu_disjointOfDiffUnion)
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u ≤ ⊥
⊢ u = ∅

Tactic:
simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h_disj

Premises used: Set.le_eq_subset, Set.bot_eq_empty, Set.subset_empty_iff
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u = ∅
⊢ False

Tactic:
hC.empty_notMem_disjointOfDiffUnion hs hI ?_

Premises used: MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u = ∅
refine : ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
⊢ False

Tactic:
refine hC.empty_notMem_disjointOfDiffUnion hs hI ?_

Premises used: MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiffUnion
-- 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
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
h_disj : u = ∅
rwa rwa₁ rwa₂ rwa₃ :
  ∀ (hu_disjointOfDiffUnion : ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI) (h_disj : u = ∅),
    ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI
⊢ ∅ ∈ hC.disjointOfDiffUnion (C := C) (s := s) hs hI

Tactic:
rwa [h_disj] at hu_disjointOfDiffUnion
-- 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
rw :
  (↑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)
⊢ ((↑I : Set (Set α)) ∪ (↑(hC.disjointOfDiffUnion (C := C) (s := s) hs hI) : Set (Set α))).PairwiseDisjoint id

Tactic:
rw [pairwiseDisjoint_union]

Premises used: Set.pairwiseDisjoint_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
h_dis : (↑I : Set (Set α)).PairwiseDisjoint id
⊢ (↑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:
⟨h_dis, hC.pairwiseDisjoint_disjointOfDiffUnion hs hI, fun u hu v hv _ ↦ ?_⟩

Premises used: And.intro, MeasureTheory.IsSetSemiring.pairwiseDisjoint_disjointOfDiffUnion