-- Mathlib/MeasureTheory/SetSemiring.lean
/-- In a semiring of sets `C`, for all set `s ∈ C` and finite set of sets `I ⊆ C`, there is a
finite set of sets in `C` whose union is `s \ ⋃₀ I`.
See `IsSetSemiring.disjointOfDiffUnion` for a definition that gives such a set. -/
lemma exists_disjoint_finset_diff_eq (hC : IsSetSemiring C) (hs : s ∈ C) (hI : ↑I ⊆ C) :
    ∃ J : Finset (Set α), ↑J ⊆ C ∧ PairwiseDisjoint (J : Set (Set α)) id ∧
      s \ ⋃₀ I = ⋃₀ J

Proof state:
case empty
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑∅ ⊆ C
⊢ ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s = ⋃₀ ↑J

Tactic:
refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩

Result:
case empty
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑∅ ⊆ C
⊢ (↑{s}).PairwiseDisjoint id ∧ s = ⋃₀ ↑{s}

Proof state:
case insert.intro.intro.intro.refine_2
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝ : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
⊢ ⋃ i ∈ J, i \ t = ⋃ i', ⋃ i, ⋃ (i_1 : i' ∈ J), ⋃ (_ : i ∈ Ju i' ⋯), i

Tactic:
refine iUnion_congr fun i ↦ ?_

Result:
case insert.intro.intro.intro.refine_2
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝ : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
i : Set α
⊢ ⋃ (_ : i ∈ J), i \ t = ⋃ i_1, ⋃ (i_2 : i ∈ J), ⋃ (_ : i_1 ∈ Ju i ⋯), i_1

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝² : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
x : { x // x ∈ J }
a✝¹ : x ∈ ↑J.attach
y : { x // x ∈ J }
a✝ : y ∈ ↑J.attach
hxy : x ≠ y
h_contra : ¬Disjoint ↑x ↑y
⊢ x = y

Tactic:
refine Subtype.ext ?_

Result:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝² : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
x : { x // x ∈ J }
a✝¹ : x ∈ ↑J.attach
y : { x // x ∈ J }
a✝ : y ∈ ↑J.attach
hxy : x ≠ y
h_contra : ¬Disjoint ↑x ↑y
⊢ ↑x = ↑y

Proof state:
case insert.intro.intro.intro.refine_2
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝ : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
⊢ s \ ⋃₀ ↑(insert t I') = ⋃₀ ↑J'

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

Result:
case insert.intro.intro.intro.refine_2
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
t : Set α
I' : Finset (Set α)
a✝ : t ∉ I'
h : ↑I' ⊆ C → ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I' = ⋃₀ ↑J
hI : insert t ↑I' ⊆ C
ht : t ∈ C
J : Finset (Set α)
h_ss : ↑J ⊆ C
h_dis : (↑J).PairwiseDisjoint id
h_eq : s \ ⋃₀ ↑I' = ⋃₀ ↑J
Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun u hu => hC.disjointOfDiff hu ht
hJu_subset : ∀ (u : Set α) (hu : u ∈ C), ↑(Ju u hu) ⊆ C
hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu)).PairwiseDisjoint id
hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ ↑(Ju u hu) = u \ t
hJu_disj' : ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C), Disjoint u v → Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))
J' : Finset (Set α) := Finset.univ.biUnion fun u => Ju ↑u ⋯
hJ'_subset : ↑J' ⊆ C
⊢ ⋃₀ ↑J \ t = ⋃₀ ↑J'