-- 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
α : 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 ∈ ↑Finset.univ, ↑(Ju ↑x ⋯)).PairwiseDisjoint id

Tactic:
refine PairwiseDisjoint.biUnion ?_ ?_

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
⊢ (↑Finset.univ).PairwiseDisjoint fun i' => ⨆ i ∈ ↑(Ju ↑i' ⋯), id i

case insert.intro.intro.intro.refine_1.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 ∈ ↑Finset.univ, (↑(Ju ↑i ⋯)).PairwiseDisjoint id

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 : Set α
⊢ ∀ (x : Set α) (h : x ∈ J), u ∈ Ju x ⋯ → u ∈ C

Tactic:
intro v hv huvt

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

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:
exact h_dis.elim x.prop y.prop h_contra

Result:
no goals