-- Mathlib/MeasureTheory/SetSemiring.lean
lemma disjoint_disjointOfDiffUnion (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    Disjoint I (hC.disjointOfDiffUnion hs hI)

Proof state:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
⊢ False

Tactic:
have h_disj : u ≤ ⊥ :=
  hC.disjoint_sUnion_disjointOfDiffUnion hs hI (subset_sUnion_of_mem huI)
  (subset_sUnion_of_mem hu_disjointOfDiffUnion)

Result:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u ≤ ⊥
⊢ False

Proof state:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u ≤ ⊥
⊢ False

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

Result:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ False

Proof state:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ ∅ ∈ hC.disjointOfDiffUnion hs hI

Tactic:
rwa [h_disj] at hu_disjointOfDiffUnion

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ¬Disjoint I (hC.disjointOfDiffUnion hs hI)
⊢ False

Tactic:
rw [Finset.not_disjoint_iff] at h

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion hs hI
⊢ False

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ∃ a ∈ I, a ∈ hC.disjointOfDiffUnion hs hI
⊢ False

Tactic:
obtain ⟨u, huI, hu_disjointOfDiffUnion⟩ := h

Result:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
⊢ False

Proof state:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ False

Tactic:
refine hC.empty_nmem_disjointOfDiffUnion hs hI ?_

Result:
case intro.intro
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
u : Set α
huI : u ∈ I
hu_disjointOfDiffUnion : u ∈ hC.disjointOfDiffUnion hs hI
h_disj : u = ∅
⊢ ∅ ∈ hC.disjointOfDiffUnion hs hI

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ Disjoint I (hC.disjointOfDiffUnion hs hI)

Tactic:
by_contra h

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
h : ¬Disjoint I (hC.disjointOfDiffUnion hs hI)
⊢ False