-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
s : Set α
I : Finset (Set α)
hC : IsSetSemiring C
hs : s ∈ C
hI : (↑I : Set (Set α)) ⊆ C
empty :
  ∀ (hI : (↑∅ : Set (Set α)) ⊆ C),
    ∃ (J : Finset (Set α)),
      (↑J : Set (Set α)) ⊆ C ∧
        (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑∅ : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert insert₁ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : (↑(Insert.insert t I') : Set (Set α)) ⊆ C),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧
              s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₂ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧
              s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₃ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧
              s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₄ insert₅ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        ∃ (J : Finset (Set α)),
          (↑J : Set (Set α)) ⊆ C ∧
            (↑J : Set (Set α)).PairwiseDisjoint id ∧
              s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₆ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C),
          ∃ (J : Finset (Set α)),
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧
                s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₇ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id),
          ∃ (J : Finset (Set α)),
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧
                s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₈ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id)
          (hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t),
          ∃ (J : Finset (Set α)),
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧
                s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₉ insert₁₀ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id)
          (hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t)
          (hJu_disj' :
            ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
              Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))),
          ∃ (J : Finset (Set α)),
            (↑J : Set (Set α)) ⊆ C ∧
              (↑J : Set (Set α)).PairwiseDisjoint id ∧
                s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₁₁ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id)
          (hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t)
          (hJu_disj' :
            ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
              Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))),
          let J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯;
          ∀ (hJ'_subset : (↑J' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧
                  s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J : Set (Set α))
insert₁₂ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id)
          (hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t)
          (hJu_disj' :
            ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
              Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))),
          let J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯;
          ∀ (hJ'_subset : (↑J' : Set (Set α)) ⊆ C), (↑J' : Set (Set α)).PairwiseDisjoint id
insert₁₃ insert₁₄ :
  ∀ (t : Set α) (I' : Finset (Set α)),
    t ∉ I' →
      ∀
        (h :
          ∀ (hI : (↑I' : Set (Set α)) ⊆ C),
            ∃ (J : Finset (Set α)),
              (↑J : Set (Set α)) ⊆ C ∧
                (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α)))
        (hI : Insert.insert t (↑I' : Set (Set α)) ⊆ C) (ht : t ∈ C) (J : Finset (Set α)) (h_ss : (↑J : Set (Set α)) ⊆ C)
        (h_dis : (↑J : Set (Set α)).PairwiseDisjoint id) (h_eq : s \ ⋃₀ (↑I' : Set (Set α)) = ⋃₀ (↑J : Set (Set α))),
        let Ju : (u : Set α) → u ∈ C → Finset (Set α) := fun (u : Set α) (hu : u ∈ C) ↦
          hC.disjointOfDiff (C := C) (s := u) (t := t) hu ht;
        ∀ (hJu_subset : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)) ⊆ C)
          (hJu_disj : ∀ (u : Set α) (hu : u ∈ C), (↑(Ju u hu) : Set (Set α)).PairwiseDisjoint id)
          (hJu_sUnion : ∀ (u : Set α) (hu : u ∈ C), ⋃₀ (↑(Ju u hu) : Set (Set α)) = u \ t)
          (hJu_disj' :
            ∀ (u : Set α) (hu : u ∈ C) (v : Set α) (hv : v ∈ C) (_h_dis : Disjoint u v),
              Disjoint (⋃₀ (↑(Ju u hu) : Set (Set α))) (⋃₀ (↑(Ju v hv) : Set (Set α)))),
          let J' : Finset (Set α) := Finset.biUnion Finset.univ fun (u : ↥J) ↦ Ju (↑u : Set α) ⋯;
          ∀ (hJ'_subset : (↑J' : Set (Set α)) ⊆ C),
            s \ ⋃₀ (↑(Insert.insert t I') : Set (Set α)) = ⋃₀ (↑J' : Set (Set α))
⊢ ∃ (J : Finset (Set α)),
    (↑J : Set (Set α)) ⊆ C ∧ (↑J : Set (Set α)).PairwiseDisjoint id ∧ s \ ⋃₀ (↑I : Set (Set α)) = ⋃₀ (↑J : Set (Set α))

Tactic:
classical
  induction I using Finset.induction with
  | empty =>
    simp only [coe_empty, sUnion_empty, diff_empty]
    refine ⟨{s}, singleton_subset_set_iff.mpr hs, ?_⟩
    simp only [coe_singleton, pairwiseDisjoint_singleton, sUnion_singleton,
      and_self_iff]
  | insert t I' _ h => ?_
  rw [coe_insert] at hI
  have ht : t ∈ C := hI (Set.mem_insert _ _)
  obtain ⟨J, h_ss, h_dis, h_eq⟩ := h ((Set.subset_insert _ _).trans hI)
  let Ju : ∀ u ∈ C, Finset (Set α) := fun u hu ↦ hC.disjointOfDiff hu ht
  have hJu_subset : ∀ (u) (hu : u ∈ C), ↑(Ju u hu) ⊆ C := by
    intro u hu x hx
    exact hC.subset_disjointOfDiff hu ht hx
  have hJu_disj : ∀ (u) (hu : u ∈ C), (Ju u hu : Set (Set α)).PairwiseDisjoint id := fun u hu ↦
    hC.pairwiseDisjoint_disjointOfDiff hu ht
  have hJu_sUnion : ∀ (u) (hu : u ∈ C), ⋃₀ (Ju u hu : Set (Set α)) = u \ t :=
    fun u hu ↦ hC.sUnion_disjointOfDiff hu ht
  have hJu_disj' : ∀ (u) (hu : u ∈ C) (v) (hv : v ∈ C) (_h_dis : Disjoint u v),
      Disjoint (⋃₀ (Ju u hu : Set (Set α))) (⋃₀ ↑(Ju v hv)) := by
    intro u hu v hv huv_disj
    rw [hJu_sUnion, hJu_sUnion]
    exact disjoint_of_subset Set.diff_subset Set.diff_subset huv_disj
  let J' : Finset (Set α) := Finset.biUnion (Finset.univ : Finset J) fun u ↦ Ju u (h_ss u.prop)
  have hJ'_subset : ↑J' ⊆ C := by
    intro u
    simp only [J', univ_eq_attach, coe_biUnion, mem_coe, mem_attach, iUnion_true,
      mem_iUnion, Finset.exists_coe, exists₂_imp]
    intro v hv huvt
    exact hJu_subset v (h_ss hv) huvt
  refine ⟨J', hJ'_subset, ?_, ?_⟩
  · rw [Finset.coe_biUnion]
    refine PairwiseDisjoint.biUnion ?_ ?_
    · simp only [univ_eq_attach, mem_coe, id, iSup_eq_iUnion]
      simp_rw [PairwiseDisjoint, Set.Pairwise]
      intro x _ y _ hxy
      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
      convert! hJu_disj' (x : Set α) (h_ss x.prop) y (h_ss y.prop) hxy_disj
      · rw [sUnion_eq_biUnion]
        congr
      · rw [sUnion_eq_biUnion]
        congr
    · exact fun u _ ↦ hJu_disj _ _
  · rw [coe_insert, sUnion_insert, Set.union_comm, ← Set.diff_diff, h_eq]
    simp_rw [J', sUnion_eq_biUnion, Set.iUnion_diff]
    simp only [mem_coe, Finset.mem_biUnion, Finset.mem_univ,
      Finset.exists_coe, iUnion_exists, true_and]
    rw [iUnion_comm]
    refine iUnion_congr fun i ↦ ?_
    by_cases hi : i ∈ J
    · simp only [hi, iUnion_true]
      rw [← hJu_sUnion i (h_ss hi), sUnion_eq_biUnion]
      simp only [mem_coe]
    · simp only [hi, iUnion_of_empty, iUnion_empty]

Premises used: Finset.mem_univ, Finset.coe_biUnion, Finset.coe_singleton, Finset.coe_empty, Set.PairwiseDisjoint, Set.sUnion_insert, Set.iSup_eq_iUnion, Set.PairwiseDisjoint.biUnion, Set.iUnion_diff, id, Set.sUnion_singleton, Insert.insert, Set.union_comm, Set.diff_empty, Set.Pairwise, Set.sUnion_eq_biUnion, Set.iUnion_of_empty, Finset.univ_eq_attach, Set.iUnion_comm, Set.diff_diff, Set.iUnion_congr, Set.iUnion_true, Set.iUnion_exists, and_self_iff, Set.iUnion_empty, Finset.coe_insert, Set.pairwiseDisjoint_singleton, Finset.exists_coe, Finset.mem_coe, Set.sUnion_empty, Finset.mem_biUnion, true_and