-- Mathlib/MeasureTheory/SetSemiring.lean
lemma nmem_disjointOfDiff (hC : IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C) :
    t ∉ hC.disjointOfDiff hs ht

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t ≤ ⊥
⊢ False

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

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ False

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ t ⊆ s \ t

Tactic:
rw [← hC.sUnion_disjointOfDiff hs ht]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ t ⊆ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
⊢ False

Tactic:
have h := @disjoint_sdiff_self_right _ t s _

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : Disjoint t (s \ t)
⊢ False

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ t ⊆ ⋃₀ ↑(hC.disjointOfDiff hs ht)

Tactic:
exact subset_sUnion_of_mem hs_mem

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ False

Tactic:
refine hC.empty_nmem_disjointOfDiff hs ht ?_

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ ∅ ∈ hC.disjointOfDiff hs ht

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t = ∅
⊢ ∅ ∈ hC.disjointOfDiff hs ht

Tactic:
rwa [← h]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
⊢ t ∉ hC.disjointOfDiff hs ht

Tactic:
intro hs_mem

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ False

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : Disjoint t (s \ t)
⊢ False

Tactic:
specialize h le_rfl this

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
this : t ⊆ s \ t
h : t ≤ ⊥
⊢ False

Proof state:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ 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_nmem_disjointOfDiff hs ht ?_
  rwa [← h]

Result:
α : Type u_1
C : Set (Set α)
s t : Set α
hC : IsSetSemiring C
hs : s ∈ C
ht : t ∈ C
hs_mem : t ∈ hC.disjointOfDiff hs ht
⊢ t ⊆ s \ t