-- Module: Mathlib.MeasureTheory.SetSemiring
Goal:
α : Type u_1
C : Set (Set α)
J : Finset (Set α)
hC : IsSetSemiring C
h1 : (↑J : Set (Set α)) ⊆ C
empty :
  ∀ (h1 : (↑∅ : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑∅ : Set (Set α)).PairwiseDisjoint K ∧
        (∀ (i : Set α), Membership.mem (γ := Finset (Set α)) ∅ i → (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α)
              (⋃ (x : Set α), ⋃ (_ : Membership.mem (γ := Finset (Set α)) ∅ x), (↑(K x) : Set (Set α))) id ∧
            (∀ (j : Set α), Membership.mem (γ := Finset (Set α)) ∅ j → ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ (j : Set α), Membership.mem (γ := Finset (Set α)) ∅ j → ∅ ∉ K j) ∧
                ⋃₀ (↑∅ : Set (Set α)) =
                  ⋃₀ ⋃ (x : Set α), ⋃ (_ : Membership.mem (γ := Finset (Set α)) ∅ x), (↑(K x) : Set (Set α))
cons :
  ∀ (s : Set α) (J : Finset (Set α)) (hJ : s ∉ J)
    (hind :
      ∀ (h1 : (↑J : Set (Set α)) ⊆ C),
        ∃ (K : Set α → Finset (Set α)),
          (↑J : Set (Set α)).PairwiseDisjoint K ∧
            (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
              PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
                (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
                  (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α)))
    (h1 : (↑(Finset.cons s J hJ) : Set (Set α)) ⊆ C),
    ∃ (K : Set α → Finset (Set α)),
      (↑(Finset.cons s J hJ) : Set (Set α)).PairwiseDisjoint K ∧
        (∀ i ∈ Finset.cons s J hJ, (↑(K i) : Set (Set α)) ⊆ C) ∧
          PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))) id ∧
            (∀ j ∈ Finset.cons s J hJ, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
              (∀ j ∈ Finset.cons s J hJ, ∅ ∉ K j) ∧
                ⋃₀ (↑(Finset.cons s J hJ) : Set (Set α)) = ⋃₀ ⋃ x ∈ Finset.cons s J hJ, (↑(K x) : Set (Set α))
⊢ ∃ (K : Set α → Finset (Set α)),
    (↑J : Set (Set α)).PairwiseDisjoint K ∧
      (∀ i ∈ J, (↑(K i) : Set (Set α)) ⊆ C) ∧
        PairwiseDisjoint.{u_1, u_1} (α := Set α) (⋃ x ∈ J, (↑(K x) : Set (Set α))) id ∧
          (∀ j ∈ J, ⋃₀ (↑(K j) : Set (Set α)) ⊆ j) ∧
            (∀ j ∈ J, ∅ ∉ K j) ∧ ⋃₀ (↑J : Set (Set α)) = ⋃₀ ⋃ x ∈ J, (↑(K x) : Set (Set α))

Tactic:
induction J using Finset.cons_induction with
  | empty => simp
  | cons s J hJ hind =>
    rw [cons_eq_insert, coe_insert, Set.insert_subset_iff] at h1
    obtain ⟨K, hK0, ⟨hK1, hK2, hK3, hK4, hK5⟩⟩ := hind h1.2
    let K1 : Set α → Finset (Set α) := fun (t : Set α) ↦
      if t = s then (hC.disjointOfDiffUnion h1.1 h1.2) else K t
    have hK1s : K1 s = hC.disjointOfDiffUnion h1.1 h1.2 := by simp [K1]
    have hK1_of_ne t (ht : t ≠ s) : K1 t = K t := by simp [K1, ht]
    use K1
    simp only [cons_eq_insert,
      mem_coe, Finset.mem_insert, sUnion_subset_iff,
      forall_eq_or_imp, coe_insert, sUnion_insert]
    -- two simplification rules for induction hypothesis
    have ht1' : ∀ x ∈ J, K1 x = K x := fun x hx ↦ hK1_of_ne _ (fun h_eq ↦ hJ (h_eq ▸ hx))
    have ht2 : (⋃ x ∈ J, (K1 x : Set (Set α))) = ⋃ x ∈ J, ((K x : Set (Set α))) := by
      apply iUnion₂_congr
      intro x hx
      exact_mod_cast hK1_of_ne _ (ne_of_mem_of_not_mem hx hJ)
    simp only [hK1s]
    refine ⟨?_, ⟨hC.disjointOfDiffUnion_subset h1.1 h1.2, ?_⟩, ?_,
      ⟨hC.subset_of_mem_disjointOfDiffUnion h1.1 h1.2, ?_⟩, ?_, ?_⟩
    · apply Set.Pairwise.insert
      · intro j hj i hi hij
        rw [Function.onFun, ht1' j hj, ht1' i hi]
        exact hK0 hj hi hij
      · intro i hi _
        have h7 : Disjoint ↑(hC.disjointOfDiffUnion h1.1 h1.2) (K i : Set (Set α)) := by
          refine disjoint_of_sSup_disjoint_of_le_of_le
            (hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2) ?_
            (@disjoint_sdiff_left _ (⋃₀ J) s) (Or.inl
              (hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2))
          simp only [mem_coe, Set.le_eq_subset]
          apply sUnion_subset_iff.mp
          exact (hK3 i hi).trans (subset_sUnion_of_mem hi)
        have h8 : Function.onFun Disjoint K1 s i := by
          refine Finset.disjoint_iff_inter_eq_empty.mpr ?_
          rw [ht1' i hi, hK1s]
          rw [Set.disjoint_iff_inter_eq_empty] at h7
          exact_mod_cast h7
        exact ⟨h8, Disjoint.symm h8⟩
    · intro i hi
      rw [ht1' i hi]
      exact hK1 i hi
    · simp only [iUnion_iUnion_eq_or_left]
      refine pairwiseDisjoint_union.mpr ⟨?_, ?_, ?_⟩
      · rw [hK1s]
        exact hC.pairwiseDisjoint_disjointOfDiffUnion h1.1 h1.2
      · simpa [ht2]
      · simp only [mem_coe, mem_iUnion, exists_prop, ne_eq, id_eq, forall_exists_index, and_imp]
        intro i hi j x hx h3 h4
        obtain ki : i ⊆ s \ ⋃₀ J := hC.subset_of_diffUnion_disjointOfDiffUnion h1.1 h1.2 _
          (hK1s ▸ hi)
        obtain hx2 : j ⊆ x := subset_trans (subset_sUnion_of_mem (ht1' x hx ▸ h3)) (hK3 x hx)
        obtain kj : j ⊆ ⋃₀ J := hx2.trans <| subset_sUnion_of_mem hx
        exact disjoint_of_subset ki kj disjoint_sdiff_left
    · intro a ha
      simp_rw [hK1_of_ne _ (ne_of_mem_of_not_mem ha hJ)]
      change ∀ t' ∈ (K a : Set (Set α)), t' ⊆ a
      rw [← sUnion_subset_iff]
      exact hK3 a ha
    · refine ⟨hC.empty_notMem_disjointOfDiffUnion h1.1 h1.2, ?_⟩
      intro a ha
      rw [ht1' a ha]
      exact hK4 a ha
    · simp only [iUnion_iUnion_eq_or_left, sUnion_union, ht2, K1]
      simp_rw [apply_ite, hK5,
      ← hC.diff_sUnion_eq_sUnion_disjointOfDiffUnion h1.1 h1.2, hK5]
      simp only [↓reduceIte, diff_union_self]

Premises used: Iff.mpr, Function.onFun, Finset.cons, Set.Pairwise.insert, and_imp, Set.sUnion_insert, Set.mem_iUnion, forall_exists_index, apply_ite, Set.diff_union_self, Finset.mem_insert, forall_eq_or_imp, exists_prop, ne_eq, Set.sUnion_subset_iff, Set.insert_subset_iff, Set.iUnion_iUnion_eq_or_left, Finset.cons_eq_insert, And.intro, reduceIte, Set.sUnion_union, Set.pairwiseDisjoint_union, Finset.coe_insert, Finset.mem_coe, id_eq