-- 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:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : ↑I ⊆ C
⊢ ∃ J, ↑J ⊆ C ∧ (↑J).PairwiseDisjoint id ∧ s \ ⋃₀ ↑I = ⋃₀ ↑J

Tactic:
induction I using Finset.induction with
| empty =>
  simp only [coe_empty, sUnion_empty, diff_empty, exists_prop]
  refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
  simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton, eq_self_iff_true,
    and_self_iff]
| @insert t I' _ h => ?_

Result:
case insert
α : 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
⊢ ∃ 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
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
⊢ Disjoint (⋃₀ ↑(Ju u hu)) (⋃₀ ↑(Ju v hv))

Tactic:
rw [hJu_sUnion, hJu_sUnion]

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
u : Set α
hu : u ∈ C
v : Set α
hv : v ∈ C
huv_disj : Disjoint u v
⊢ Disjoint (u \ t) (v \ t)

Proof state:
case h.e'_5
α : 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) y = ⋃ i ∈ ↑(Ju ↑y ⋯), i

Tactic:
congr

Result:
no goals

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

Tactic:
convert hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj

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 = ⋃₀ ↑(Ju ↑x ⋯)

case h.e'_5
α : 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) y = ⋃₀ ↑(Ju ↑y ⋯)