-- 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 insert.intro.intro.intro.refine_1.refine_1
α : 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
⊢ Function.onFun Disjoint (fun i' => ⋃ i ∈ Ju ↑i' ⋯, i) x y

Tactic:
have hxy_disj : Disjoint (x : Set α) y := by
  by_contra h_contra
  refine hxy ?_
  refine Subtype.ext ?_
  exact h_dis.elim x.prop y.prop h_contra

Result:
case insert.intro.intro.intro.refine_1.refine_1
α : 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
hxy_disj : Disjoint ↑x ↑y
⊢ Function.onFun Disjoint (fun i' => ⋃ i ∈ Ju ↑i' ⋯, i) x y

Proof state:
case insert.intro.intro.intro
α : 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
⊢ ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑(insert t I') = ⋃₀ ↑J

Tactic:
have hJu_subset : ∀ (u) (hu : u ∈ C), ↑(Ju u hu) ⊆ C := by
  intro u hu x hx
  exact hC.subset_disjointOfDiff hu ht hx

Result:
case insert.intro.intro.intro
α : 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
⊢ ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑(insert t I') = ⋃₀ ↑J

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 ⋯
u v : Set α
hv : v ∈ J
huvt : u ∈ Ju v ⋯
⊢ u ∈ C

Tactic:
exact hJu_subset v (h_ss hv) huvt

Result:
no goals

Proof state:
case h.e'_4
α : 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
hxy_disj : Disjoint ↑x ↑y
⊢ (fun i' => ⋃ i ∈ Ju ↑i' ⋯, i) x = ⋃₀ ↑(Ju ↑x ⋯)

Tactic:
rw [sUnion_eq_biUnion]

Result:
case h.e'_4
α : 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
hxy_disj : Disjoint ↑x ↑y
⊢ (fun i' => ⋃ i ∈ Ju ↑i' ⋯, i) x = ⋃ i ∈ ↑(Ju ↑x ⋯), i