awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
s : Set α
hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s
T : Finset (Set α)
hTC : (↑T : Set (Set α)) ⊆ C
empty :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (hTC : (↑∅ : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ sup ∅ id)
insert :
  ∀ (t : Set α) (T : Finset (Set α)),
    t ∉ T →
      ∀
        (ih :
          ∀ ⦃s : Set α⦄
            (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
            (hTC : (↑T : Set (Set α)) ⊆ C),
            Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
              (s \ T.sup id))
        ⦃s : Set α⦄
        (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
        (hTC : (↑(Insert.insert t T) : Set (Set α)) ⊆ C),
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
          (s \ (Insert.insert t T).sup id)
⊢ Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)

Tactic:
induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC

Premises used: Finset.sup_insert, Set.sup_eq_union, id, Insert.insert, Finset.sup_sdiff_right, Set.insert_subset_iff, Set.diff_diff, Finset.coe_insert, Finset.sup'_eq_sup, rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
hC : IsSetSemiring C
rintro :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (T : Finset (Set α)) (hT : T.Nonempty) (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α))
      (s \ T.sup' hT id)
rintro₁ :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (T : Finset (Set α)) (hT : T.Nonempty) (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
rintro₂ :
  ∀ ⦃s : Set α⦄
    (hs : Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s)
    (T : Finset (Set α)) (hTC : (↑T : Set (Set α)) ⊆ C),
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ T.sup id)
⊢ ∀ ⦃s t : Set α⦄,
    Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) s →
      Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) t →
        Membership.mem (γ := Set (Set α)) ((supClosure : (a : Set (Set α)) → Set (Set α)) C : Set (Set α)) (s \ t)

Tactic:
classical
    rintro s _ hs ⟨T, hT, hTC, rfl⟩
    rw [sup'_eq_sup]
    clear hT
    induction T using Finset.induction generalizing s with
    | empty => simpa
    | insert t T _ ih =>
      simp_rw [sup_insert, id, sup_eq_union, ← diff_diff]
      rw [coe_insert, insert_subset_iff] at hTC
      obtain ⟨htC, hTC⟩ := hTC
      refine ih ?_ hTC
      obtain ⟨S, hS, hSC, rfl⟩ := hs
      rw [sup'_eq_sup, ← Finset.sup_sdiff_right]
      refine supClosed_supClosure.finsetSup_mem hS fun s hs => ?_
      exact hC.diff_mem_supClosure (hSC hs) htC

Premises used: Finset.sup_insert, Set.sup_eq_union, id, Insert.insert, Finset.sup_sdiff_right, Set.insert_subset_iff, Set.diff_diff, Finset.coe_insert, Finset.sup'_eq_sup, rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∅ ∉ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht

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

Premises used: Finset.mem_singleton, MeasureTheory.IsSetSemiring.disjointOfDiff, Finset.mem_sdiff, not_true, and_false, not_false_iff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ∅ ∉ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht

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

Premises used: Finset.mem_singleton, MeasureTheory.IsSetSemiring.disjointOfDiff, Finset.mem_sdiff, not_true, and_false, not_false_iff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
simp :
  (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) ⊆ C

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

Premises used: Finset.coe_singleton, Finset.coe_sdiff, Set.diff_singleton_subset_iff, MeasureTheory.IsSetSemiring.disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C

Tactic:
(hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, HasSubset.Subset.trans, MeasureTheory.IsSetSemiring.diff_eq_sUnion', And.left, Set.subset_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C

Tactic:
exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, HasSubset.Subset.trans, MeasureTheory.IsSetSemiring.diff_eq_sUnion', And.left, Set.subset_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
simp :
  (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
          (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
      Set (Set α)) ⊆
    insert ∅ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) ⊆ C

Tactic:
classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton, diff_singleton_subset_iff]
  exact (hC.diff_eq_sUnion' s hs t ht).choose_spec.1.trans (Set.subset_insert _ _)

Premises used: Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, Set.diff_singleton_subset_iff, HasSubset.Subset.trans, MeasureTheory.IsSetSemiring.disjointOfDiff, MeasureTheory.IsSetSemiring.diff_eq_sUnion', And.left, Set.subset_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
simp :
  ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id

Tactic:
simp only [disjointOfDiff, coe_sdiff, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id

Tactic:
Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
      diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, MeasureTheory.IsSetSemiring.diff_eq_sUnion', Set.PairwiseDisjoint.subset, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id

Tactic:
exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
      diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, MeasureTheory.IsSetSemiring.diff_eq_sUnion', Set.PairwiseDisjoint.subset, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
simp :
  ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}).PairwiseDisjoint
    id
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id

Tactic:
classical
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  exact Set.PairwiseDisjoint.subset (hC.diff_eq_sUnion' s hs t ht).choose_spec.2.1
      diff_subset

Premises used: Set.diff_subset, Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiff, MeasureTheory.IsSetSemiring.diff_eq_sUnion', Set.PairwiseDisjoint.subset, And.right, And.left
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
rw :
  ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s \ t

Tactic:
rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]

Premises used: Exists.choose_spec, MeasureTheory.IsSetSemiring.diff_eq_sUnion', And.right
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
simp :
  ⋃₀
      ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))

Tactic:
simp only [disjointOfDiff, coe_sdiff, coe_singleton]

Premises used: Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
rw rw₁ :
  ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀
      ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : 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 t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
rw rw₁ rw₂ :
  ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
rw₃ :
  ⋃₀
      ((↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
              (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
          Set (Set α)) \
        {∅}) =
    ⋃₀
      (↑(⋯.choose (p := fun (I : Finset (Set α)) ↦
            (↑I : Set (Set α)) ⊆ C ∧ (↑I : Set (Set α)).PairwiseDisjoint id ∧ s \ t = ⋃₀ (↑I : Set (Set α)))) :
        Set (Set α))
⊢ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s \ t

Tactic:
classical
  rw [(hC.diff_eq_sUnion' s hs t ht).choose_spec.2.2]
  simp only [disjointOfDiff, coe_sdiff, coe_singleton]
  rw [sUnion_diff_singleton_empty]

Premises used: Exists.choose_spec, Finset.coe_singleton, Finset.coe_sdiff, MeasureTheory.IsSetSemiring.disjointOfDiff, MeasureTheory.IsSetSemiring.diff_eq_sUnion', And.right, Set.sUnion_diff_singleton_empty
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
⊢ Disjoint t (s \ t)

Tactic:
have h := @disjoint_sdiff_self_right _ t s _
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : Disjoint t (s \ t)
⊢ t ≤ ⊥

Tactic:
specialize h le_rfl this

Premises used: le_rfl
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t ≤ ⊥
⊢ t = ∅

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

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 t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ False

Tactic:
hC.empty_notMem_disjointOfDiff hs ht ?_

Premises used: MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t = ∅
refine : ∅ ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ False

Tactic:
refine hC.empty_notMem_disjointOfDiff hs ht ?_

Premises used: MeasureTheory.IsSetSemiring.empty_notMem_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
this : t ⊆ s \ t
h : t = ∅
rwa rwa₁ rwa₂ rwa₃ : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ ∅ ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht

Tactic:
rwa [← h]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
suffices : t ⊆ s \ t
⊢ False

Tactic:
suffices t ⊆ s \ t by
    have h := @disjoint_sdiff_self_right _ t s _
    specialize h le_rfl this
    simp only [Set.bot_eq_empty, Set.le_eq_subset, subset_empty_iff] at h
    refine hC.empty_notMem_disjointOfDiff hs ht ?_
    rwa [← h]
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
rw : t ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ t ⊆ s \ t

Tactic:
rw [← hC.sUnion_disjointOfDiff hs ht]

Premises used: MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ t ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))

Tactic:
subset_sUnion_of_mem hs_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht
⊢ t ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))

Tactic:
exact subset_sUnion_of_mem hs_mem

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
rw : t ∪ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
| s

Tactic:
rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]

Premises used: MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
conv_rhs :
  ⋃₀ insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    t ∪ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ ⋃₀ insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) = s

Tactic:
conv_rhs => rw [← union_diff_cancel hst, ← hC.sUnion_disjointOfDiff hs ht]

Premises used: MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff, Set.union_diff_cancel
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hst : t ⊆ s
⊢ ⋃₀ insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)) =
    t ∪ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))

Tactic:
simp only [sUnion_insert]

Premises used: Set.sUnion_insert
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
rw : Disjoint t (s \ t)
⊢ Disjoint t (⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)))

Tactic:
rw [hC.sUnion_disjointOfDiff]

Premises used: MeasureTheory.IsSetSemiring.sUnion_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (s \ t)

Tactic:
disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ Disjoint t (s \ t)

Tactic:
exact disjoint_sdiff_right

Premises used: Set.disjoint_sdiff_right
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id

Tactic:
have h := hC.pairwiseDisjoint_disjointOfDiff hs ht
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
⊢ (insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))).PairwiseDisjoint id

Tactic:
PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_

Premises used: MeasureTheory.IsSetSemiring.notMem_disjointOfDiff, Set.PairwiseDisjoint.insert_of_notMem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
refine :
  ∀ (u : Set α) (hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))), Disjoint (id t) (id u)
⊢ (insert t (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))).PairwiseDisjoint id

Tactic:
refine PairwiseDisjoint.insert_of_notMem h (hC.notMem_disjointOfDiff hs ht) fun u hu ↦ ?_

Premises used: MeasureTheory.IsSetSemiring.notMem_disjointOfDiff, Set.PairwiseDisjoint.insert_of_notMem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
simp_rw : Disjoint t u
⊢ Disjoint (id t) (id u)

Tactic:
simp_rw [id]

Premises used: id
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ Disjoint t u

Tactic:
Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)

Premises used: Disjoint.mono_right, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
refine : u ≤ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ Disjoint t u

Tactic:
refine Disjoint.mono_right ?_ (hC.disjoint_sUnion_disjointOfDiff hs ht)

Premises used: Disjoint.mono_right, MeasureTheory.IsSetSemiring.disjoint_sUnion_disjointOfDiff
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ u ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))

Tactic:
subset_sUnion_of_mem hu

Premises used: Set.subset_sUnion_of_mem
-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
h : (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α)).PairwiseDisjoint id
u : Set α
hu : u ∈ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))
⊢ u ⊆ ⋃₀ (↑(hC.disjointOfDiff (C := C) (s := s) (t := t) hs ht) : Set (Set α))

Tactic:
exact subset_sUnion_of_mem hu

Premises used: Set.subset_sUnion_of_mem