feat: The finite product of semi-rings (in terms of measure theory) is a semi-ring.

Mathlib/Data/Set/Pairwise/Lattice.lean

@@ -55,6 +55,14 @@ theorem pairwiseDisjoint_sUnion {s : Set (Set ι)} (h : DirectedOn (· ⊆ ·) s
     (⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a⦄, a ∈ s → Set.PairwiseDisjoint a f :=
   pairwise_sUnion h
 
+theorem pairwiseDisjoint_union_of_disjoint
+    {s t : Set (Set ι)} {f : Set ι → α} (hf : Monotone f)
+    (hs : PairwiseDisjoint s f) (ht : PairwiseDisjoint t f)
+    (hst : Disjoint (f (Set.sUnion s)) (f (sUnion t))) : PairwiseDisjoint (s ∪ t) f := by
+  refine pairwiseDisjoint_union.mpr ⟨hs, ht, fun a ha b hb hab ↦ ?_⟩
+  apply hst.mono (hf (subset_sUnion_of_subset s a (subset_refl a) ha))
+    (hf (subset_sUnion_of_subset t b (subset_refl b) hb))
+
 end PartialOrderBot
 
 section CompleteLattice

Mathlib/Data/Set/Prod.lean

@@ -5,6 +5,7 @@ Authors: Mario Carneiro, Johannes Hölzl, Patrick Massot
 -/
 import Mathlib.Data.Set.Image
 import Mathlib.Data.SProd
+import Mathlib.Tactic.NthRewrite
 
 /-!
 # Sets in product and pi types
@@ -732,6 +733,17 @@ theorem pi_if {p : ι → Prop} [h : DecidablePred p] (s : Set ι) (t₁ t₂ :
 theorem union_pi : (s₁ ∪ s₂).pi t = s₁.pi t ∩ s₂.pi t := by
   simp [pi, or_imp, forall_and, setOf_and]
 
+theorem pi_antitone (h : s₁ ⊆ s₂) : s₂.pi t ⊆ s₁.pi t := by
+  rw [← union_diff_cancel h, union_pi]
+  exact Set.inter_subset_left
+
+open scoped Classical in
+lemma union_pi_ite_of_disjoint {s t : Set ι} {x y : (i : ι) → Set (α i)} (hst : Disjoint s t) :
+((s ∪ t).pi fun i ↦ if i ∈ s then x i else y i)  = (s.pi x) ∩ (t.pi y) := by
+ rw [union_pi, Set.pi_congr rfl (fun i hi ↦ if_pos hi), Set.pi_congr rfl (fun i hi ↦
+    if_neg <| hst.symm.not_mem_of_mem_left hi)]
+
+
 theorem union_pi_inter
     (ht₁ : ∀ i ∉ s₁, t₁ i = univ) (ht₂ : ∀ i ∉ s₂, t₂ i = univ) :
     (s₁ ∪ s₂).pi (fun i ↦ t₁ i ∩ t₂ i) = s₁.pi t₁ ∩ s₂.pi t₂ := by
@@ -893,6 +905,25 @@ theorem univ_pi_ite (s : Set ι) [DecidablePred (· ∈ s)] (t : ∀ i, Set (α
   refine forall_congr' fun i => ?_
   split_ifs with h <;> simp [h]
 
+section Setdiff
+
+/-- Write that set difference `(s ∪ t).pi x \ (s ∪ t).pi y` as a union. -/
+lemma pi_setdiff_eq_union (s t : Set ι) (x y : (i : ι) → Set (α i)) :
+  (s ∪ t).pi x \ (s ∪ t).pi y = t.pi x ∩ (s.pi x \ s.pi y) ∪ (t.pi x \ t.pi y) ∩ (s.pi x ∩ s.pi y)
+     := by
+  rw [union_pi, union_pi, diff_eq_compl_inter, compl_inter,  union_inter_distrib_right,
+    ← inter_assoc, ← diff_eq_compl_inter, ← inter_assoc, inter_comm, inter_assoc,
+    inter_comm (s.pi x ) (t.pi x), ← inter_assoc,  ← diff_eq_compl_inter, ← union_diff_self]
+  apply congrArg (Union.union (t.pi x ∩ (s.pi x \ s.pi y)))
+  aesop
+
+lemma pi_setdiff_union_disjoint (s t : Set ι) (x : (i : ι) → Set (α i)) (y : (i : ι) → Set (α i)) :
+  Disjoint (t.pi x ∩ (s.pi x \ s.pi y)) ((t.pi x \ t.pi y) ∩ (s.pi x ∩ s.pi y)) :=
+    Disjoint.symm (Disjoint.inter_left' (t.pi x \ t.pi y) (Disjoint.symm
+    (Disjoint.inter_left' (t.pi x) disjoint_sdiff_inter)))
+
+end Setdiff
+
 end Pi
 
 end Set
@@ -931,6 +962,21 @@ theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t :
 
 end Equiv
 
+section image
+
+open Set
+variable {ι ι' : Type*} {α : ι → Type*}
+
+lemma subset_pi_image_of_subset {s : Set ι} {B C : (i : ι) → Set (Set (α i))}
+    (hBC : ∀ i ∈ s, B i ⊆ C i) : s.pi  '' s.pi B ⊆ s.pi  '' s.pi C := by
+  simp only [Set.image_subset_iff]
+  intro b hb
+  simp only [Set.mem_preimage, Set.mem_image, Set.mem_pi] at hb ⊢
+  exact ⟨b, ⟨fun i a ↦ hBC i a (hb i a), rfl⟩⟩
+
+
+end image
+
 namespace Set
 
 variable {α β γ δ : Type*} {s : Set α} {f : α → β}

Mathlib/MeasureTheory/MeasurableSpace/Pi.lean

@@ -30,11 +30,17 @@ lemma MeasurableSpace.pi_eq_generateFrom_projections {mα : ∀ i, MeasurableSpa
   simp only [pi, ← generateFrom_iUnion_measurableSet, iUnion_setOf, measurableSet_comap]
 
 /-- Boxes formed by π-systems form a π-system. -/
-theorem IsPiSystem.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) :
-    IsPiSystem (pi univ '' pi univ C) := by
+theorem IsPiSystem.pi_subset {C : ∀ i, Set (Set (α i))} (s : Set ι)
+    (hC : ∀ i ∈ s, IsPiSystem (C i)) : IsPiSystem (pi s '' pi s C) := by
   rintro _ ⟨s₁, hs₁, rfl⟩ _ ⟨s₂, hs₂, rfl⟩ hst
-  rw [← pi_inter_distrib] at hst ⊢; rw [univ_pi_nonempty_iff] at hst
-  exact mem_image_of_mem _ fun i _ => hC i _ (hs₁ i (mem_univ i)) _ (hs₂ i (mem_univ i)) (hst i)
+  rw [← pi_inter_distrib] at hst ⊢; rw [pi_nonempty_iff] at hst
+  refine mem_image_of_mem _ fun i hi =>
+    hC i hi _ (hs₁ i hi) _ (hs₂ i hi) ?_
+  rcases hst i with ⟨x, a⟩
+  exact Set.nonempty_of_mem (a hi)
+
+theorem IsPiSystem.pi {C : ∀ i, Set (Set (α i))} (hC : ∀ i, IsPiSystem (C i)) :
+    IsPiSystem (pi univ '' pi univ C) := IsPiSystem.pi_subset univ (fun i _ ↦ hC i)
 
 /-- Boxes form a π-system. -/
 theorem isPiSystem_pi [∀ i, MeasurableSpace (α i)] :

Mathlib/MeasureTheory/PiSystem.lean

@@ -67,6 +67,13 @@ variable {α β : Type*}
 def IsPiSystem (C : Set (Set α)) : Prop :=
   ∀ᵉ (s ∈ C) (t ∈ C), (s ∩ t : Set α).Nonempty → s ∩ t ∈ C
 
+theorem isPiSystem_iff_of_nmem_empty {C : Set (Set α)} (hC : ∅ ∈ C) :
+    (∀ᵉ (s ∈ C) (t ∈ C), s ∩ t ∈ C) ↔ IsPiSystem C := by
+  refine ⟨fun h s hs t ht _ ↦ h s hs t ht, fun h s hs t ht ↦ ?_⟩
+  by_cases h1 :(s ∩ t).Nonempty
+  · exact h s hs t ht h1
+  · exact (not_nonempty_iff_eq_empty.mp h1) ▸ hC
+
 namespace MeasurableSpace
 
 theorem isPiSystem_measurableSet {α : Type*} [MeasurableSpace α] :

Mathlib/MeasureTheory/SetSemiring.lean

@@ -7,8 +7,9 @@ import Mathlib.Data.Nat.Lattice
 import Mathlib.Data.Set.Accumulate
 import Mathlib.Data.Set.Pairwise.Lattice
 import Mathlib.MeasureTheory.PiSystem
+import Mathlib.MeasureTheory.MeasurableSpace.Pi
 
-/-! # Semirings and rings of sets
+/-! # Semirings of sets
 
 A semi-ring of sets `C` (in the sense of measure theory) is a family of sets containing `∅`,
 stable by intersection and such that for all `s, t ∈ C`, `t \ s` is equal to a disjoint union of
@@ -19,8 +20,6 @@ is an interval (possibly empty). The union of two intervals may not be an interv
 The set difference of two intervals may not be an interval, but it will be a disjoint union of
 two intervals.
 
-A ring of sets is a set of sets containing `∅`, stable by union, set difference and intersection.
-
 ## Main definitions
 
 * `MeasureTheory.IsSetSemiring C`: property of being a semi-ring of sets.
@@ -33,8 +32,6 @@ A ring of sets is a set of sets containing `∅`, stable by union, set differenc
 * `MeasureTheory.IsSetSemiring.disjointOfUnion hJ`: for `hJ ⊆ C`, this is a
   `Finset` of pairwise disjoint sets such that `⋃₀ J = ⋃₀ hC.disjointOfUnion hJ`.
 
-* `MeasureTheory.IsSetRing`: property of being a ring of sets.
-
 ## Main statements
 
 * `MeasureTheory.IsSetSemiring.exists_disjoint_finset_diff_eq`: the existence of the `Finset` given
@@ -45,9 +42,11 @@ A ring of sets is a set of sets containing `∅`, stable by union, set differenc
   * `⋃ x ∈ J, K x` are pairwise disjoint and do not contain ∅,
   * `⋃ s ∈ K x, s ⊆ x`,
   * `⋃ x ∈ J, x = ⋃ x ∈ J, ⋃ s ∈ K x, s`.
-
+* `MeasureTheory.IsSetSemiring.pi`: For a `Finset s` and family of semirings,
+`∀ i ∈ s, IsSetSemiring (C i)`, the cartesian  product `s.pi '' s.pi C` is a semiring.
 -/
 
+
 open Finset Set
 
 namespace MeasureTheory
@@ -66,6 +65,15 @@ namespace IsSetSemiring
 
 lemma isPiSystem (hC : IsSetSemiring C) : IsPiSystem C := fun s hs t ht _ ↦ hC.inter_mem s hs t ht
 
+lemma iff (C : Set (Set α)) : IsSetSemiring C ↔
+    (∅ ∈ C ∧ IsPiSystem C ∧ ∀ s ∈ C, ∀ t ∈ C,
+    ∃ I : Finset (Set α), ↑I ⊆ C ∧ PairwiseDisjoint (I : Set (Set α)) id ∧ s \ t = ⋃₀ I) :=
+  ⟨fun hC ↦ ⟨hC.empty_mem, isPiSystem hC, hC.diff_eq_sUnion'⟩,
+    fun ⟨h1, h2, h3⟩ ↦ {
+      empty_mem := h1,
+      inter_mem := (isPiSystem_iff_of_nmem_empty h1).mpr h2,
+      diff_eq_sUnion' := h3} ⟩
+
 section disjointOfDiff
 
 open scoped Classical in
@@ -305,14 +313,10 @@ lemma sUnion_union_disjointOfDiffUnion_of_subset (hC : IsSetSemiring C) (hs : s
   rw [sUnion_union]
 
 end disjointOfDiffUnion
-
 section disjointOfUnion
 
-
 variable {j : Set α} {J : Finset (Set α)}
 
-open Set MeasureTheory Order
-
 theorem disjointOfUnion_props (hC : IsSetSemiring C) (h1 : ↑J ⊆ C) :
     ∃ K : Set α → Finset (Set α),
       PairwiseDisjoint J K
@@ -435,6 +439,182 @@ lemma sUnion_disjointOfUnion (hC : IsSetSemiring C) (hJ : ↑J ⊆ C) :
 
 end disjointOfUnion
 
+section piSemiring
+
+variable {ι : Type*} {α : ι → Type*} {C : (i : ι) → Set (Set (α i))}
+
+/-- For `K' a : Finset (Set α i))`, define the
+`Fintype (({a} : Set ι).pi  '' ({a} : Set ι).pi K')`. -/
+noncomputable
+
+def fintype_pi_ofFinset (a : ι) (K' : (i : ι) → (Set (Set (α i)))) (K : Finset (Set (α a)))
+  (hK' : K = K' a) : Fintype (({a} : Set ι).pi  '' ({a} : Set ι).pi K') := by
+  let E : Set (α a) → Set (((i : ι) → α i)) :=
+    fun (k : Set (α a)) ↦ { f : ((i : ι) → α i) | f a ∈ k }
+  have h (y : _) (hy : y ∈ (({a} : Set ι).pi  '' ({a} : Set ι).pi K')) : ∃ k ∈ K, E k = y := by
+    obtain ⟨x, hx1, hx2⟩ := hy
+    simp only [singleton_pi, Set.mem_preimage, Function.eval] at hx1
+    rw [← hK'] at hx1
+    refine ⟨x a, hx1, hx2.symm ▸ Eq.symm (singleton_pi' a x)⟩
+  simp only [mem_coe] at h
+  exact Finite.fintype <| Finite.Set.subset (E '' ↑K) h
+
+lemma pairwiseDisjoint_set_pi {a : ι} {K : (i : ι) → Set (Set (α i))}
+    (h : PairwiseDisjoint (K a) id) :
+      PairwiseDisjoint (({a} : Set ι).pi  '' ({a} : Set ι).pi K) id := by
+  intro m hm n hn hmn
+  simp only [↓reduceDIte, Set.mem_image, Set.mem_preimage,
+    mem_coe] at hm hn
+  obtain ⟨o, ho1, ho2⟩ := hm
+  obtain ⟨p, hp1, hp2⟩ := hn
+  simp only [singleton_pi, ↓reduceDIte, Function.eval, mem_coe] at ho1 hp1
+  rw [← ho2, ← hp2] at hmn ⊢
+  apply Set.Disjoint.set_pi (mem_singleton_iff.mpr rfl)
+  exact h ho1 hp1 <| fun h7 ↦  hmn <| Set.pi_congr rfl <| fun i hi ↦ (mem_singleton_iff.mpr hi) ▸ h7
+
+lemma pi_singleton_diff_eq_sUnion {a : ι} {K' : (i : ι) → Set (Set (α i))}
+  {x y : (i : ι) → Set (α i)} (hK : x a \ y a = ⋃₀ K' a) :
+      (({a} : Set ι).pi x \ ({a} : Set ι).pi y) =
+        ⋃₀ (({a} : Set ι).pi  '' ({a} : Set ι).pi K') := by
+  classical
+  simp only [sUnion_image]
+  ext z
+  simp only [singleton_pi, mem_diff, Set.mem_preimage, Function.eval, mem_iUnion, exists_prop]
+  refine ⟨fun h ↦ ?_, fun ⟨w, hw⟩ ↦ ?_⟩
+  · rw [← mem_diff, hK] at h
+    obtain ⟨w, ⟨hw1, hw2⟩⟩ := mem_sUnion.mp h
+    use fun i ↦ (if h : a = i then h ▸ w else (univ : Set (α i)))
+    simp only [↓reduceDIte]
+    exact ⟨hw1, hw2⟩
+  · rw [← mem_diff, hK, mem_sUnion]
+    use w a
+
+lemma pi_inter_image {s t : Set ι} {x : (i : ι) → Set (α i)}  (hst : Disjoint s t)
+  (hx : ∀ i ∈ t, x i ∈ C i) {K' : Set (Set ((i : ι) → α i))} (hK'1 : K' ⊆ s.pi '' s.pi C) :
+  Set.inter (t.pi x) '' K' ⊆ (s ∪ t).pi '' (s ∪ t).pi C := by
+  intro a ha
+  obtain ⟨b, ⟨hb1, hb2⟩⟩ := ha
+  have hb3 := hK'1 hb1
+  obtain ⟨c, ⟨hc1, hc2⟩⟩ := hb3
+  simp only [Set.mem_image, Set.mem_pi, Set.mem_union]
+  classical
+  use fun i ↦ if i ∈ s then c i else x i
+  refine ⟨?_, ?_⟩
+  · rintro i (hi1 | hi2)
+    · simp [hi1]
+      simp only [Set.mem_pi] at hc1
+      exact hc1 i hi1
+    · have h : i ∉ s := by
+        exact Disjoint.not_mem_of_mem_left (Disjoint.symm hst) hi2
+      simp only [h, ↓reduceIte]
+      exact hx i hi2
+  · rw [← hb2, ← hc2, union_pi_ite_of_disjoint hst, inter_comm]
+    rfl
+
+lemma pi_inter_image' {s t : Set ι} {x : (i : ι) → Set (α i)}  (hst : Disjoint s t)
+(hx : ∀ i ∈ t, x i ∈ C i) {K' : (i : ι) → Set (Set (α i))} (hK'1 : ∀ i ∈ s, K' i ⊆ C i) :
+  Set.inter (t.pi x) '' (s.pi  '' s.pi K') ⊆ (s ∪ t).pi '' (s ∪ t).pi C := by
+  exact pi_inter_image hst hx <| subset_pi_image_of_subset hK'1
+
+/- For a `Finset s` and family of semirings, `∀ i ∈ s, IsSetSemiring (C i)`, the cartesian
+product `s.pi '' s.pi C` is a semiring. -/
+theorem pi {s : Set ι} (hs : Finite s)
+    (hC : ∀ i ∈ s, IsSetSemiring (C i)) : s.Nonempty →  IsSetSemiring (s.pi '' s.pi C) := by
+  classical
+  refine Set.Finite.induction_on_subset s hs (fun h ↦ False.elim <| Set.not_nonempty_empty h) ?_
+  intro a t ha hts t_fin h_ind b; clear b
+  refine (IsSetSemiring.iff _).mpr ⟨?_, ?_, ?_⟩
+  · simp only [insert_pi, Set.mem_image, mem_inter_iff, Set.mem_pi]
+    use fun _ ↦ ∅
+    simp only [Set.preimage_empty, Set.empty_inter, and_true]
+    refine ⟨(hC a ha).empty_mem, fun i a ↦ (hC i (hts a)).empty_mem⟩
+  · exact IsPiSystem.pi_subset (insert a t)
+      (fun i hi ↦ (hC i (Set.insert_subset ha hts hi)).isPiSystem)
+  · intro u ⟨x, ⟨hx1, hx2⟩⟩ v ⟨y, ⟨hy1, hy2⟩⟩
+    simp_rw [Set.mem_pi, Set.mem_insert_iff, insert_pi, ← singleton_pi] at hx1 hx2 hy1 hy2
+    -- Write `u : Set ((i : ι) → α i)` as `x : (i : ι) → Set (α i)` with `u = {a}.pi x ∩ t.pi x`.
+    have h1 (u : Set ι) (x : (i : ι) → Set (α i)) (hu : ∀ i ∈ u, x i ∈ C i) :
+      u.pi x ∈ u.pi '' u.pi C :=
+      Set.mem_image_of_mem u.pi <| Set.mem_pi.mpr fun i hi ↦ hu i hi
+    have hx1' := h1 t x (fun i hi ↦ hx1 i (Or.inr hi))
+    have hy1' := h1 t y (fun i hi ↦ hy1 i (Or.inr hi))
+    clear h1
+    -- Express `u \ v` using `x` and `y`.
+    have h1 : u \ v = (t.pi x ∩ (({a} : Set ι).pi x \ ({a} : Set ι).pi y)) ∪
+    ((t.pi x \ t.pi y) ∩ (({a} : Set ι).pi x ∩ ({a} : Set ι).pi y)):=  by
+      rw [← hx2, ← hy2, ← union_pi, ← union_pi]
+      apply pi_setdiff_eq_union
+    -- Show that the two sets from `h1` are disjoint.
+    obtain h2 := pi_setdiff_union_disjoint ({a} : Set ι) t x y
+    -- `K : Set (Set (α a))` is such that `x a \ y a = ⋃₀ K`.
+    /- Several sets need to be constructed based on `K`.
+        We use that convention that for some set system  `X`
+        * `hX1` states that `X` is contained in the corresponding structure using the semiring;
+        * `hX2` states that the set mentioned in `hX1` is pairwise disjoint;
+        * `hX3` states that the union of sets from `hX1` is the corresponding set difference. -/
+    obtain ⟨K, ⟨hK1, hK2, hK3⟩⟩ :=
+      (hC a ha).diff_eq_sUnion' (x a) (hx1 a (Or.inl rfl)) (y a) (hy1 a (Or.inl rfl))
+    -- `K' : (i : ι) → Set (Set (α i))` satisfies `K' a = K`.
+    let K' : (i : ι) → Set (Set (α i)) :=
+      fun (i : ι) => dite (i = a) (fun h ↦ h ▸ K.toSet) (fun _ ↦ (default : Set (Set (α i))))
+    have hKK' : K = K' a := by simp only [dite_eq_ite, ↓reduceIte, K']
+    haveI hE' : Fintype (({a} : Set ι).pi  '' ({a} : Set ι).pi K')
+      := fintype_pi_ofFinset a K' K (by simp only [↓reduceDIte, K'])
+    -- have hE1 := subset_pi_image_of_subset hK'1; clear hK'1
+    have hE3 := pi_singleton_diff_eq_sUnion (hKK'.symm ▸ hK3)
+    let F := Set.inter (t.pi x) '' (({a} : Set ι).pi  '' ({a} : Set ι).pi K')
+    have hF1 : F ⊆ (insert a t).pi '' (insert a t).pi C :=
+      pi_inter_image' (Set.disjoint_singleton_left.mpr t_fin) (fun i hi ↦ hx1 i (Or.inr hi))
+        (fun i hi ↦ mem_singleton_iff.mp hi ▸ hKK' ▸ hK1)
+    have hF2 : PairwiseDisjoint F id :=
+      PairwiseDisjoint.image_of_le (pairwiseDisjoint_set_pi (hKK' ▸ hK2)) <|
+      fun a b hb ↦ Set.mem_of_mem_inter_right hb
+    have hF3 : ⋃₀ F = (t.pi x) ∩ (({a} : Set ι).pi x \ ({a} : Set ι).pi y) := by
+      simp_rw [hE3, sUnion_eq_iUnion, iUnion_coe_set, inter_iUnion₂]
+      simp only [singleton_pi, sUnion_image, Set.mem_image, Set.mem_preimage, Function.eval,
+        iUnion_exists, biUnion_and', iUnion_iUnion_eq_right, F]
+      rfl
+    by_cases h : t.Nonempty
+    rotate_left
+    · have h : t = ∅ := Set.not_nonempty_iff_eq_empty.mp h; clear h_ind
+      use F.toFinset
+      simp only [coe_union, coe_toFinset]
+      refine ⟨hF1, hF2, ?_⟩
+      simp only [h, empty_pi, Set.univ_inter, sdiff_self, Set.bot_eq_empty,
+        Set.empty_inter, Set.union_empty] at hF3 h1
+      exact hF3.symm ▸ h1
+    · have h_ind' := h_ind h; clear h h_ind
+      let G := Set.inter (({a} : Set ι).pi y ∩ ({a} : Set ι).pi x) ''
+        (h_ind'.disjointOfDiff hx1' hy1')
+      have hG1 : G ⊆ (insert a t).pi '' (insert a t).pi C := by
+        simp only [G]
+        rw [← singleton_union, union_comm, ← Set.pi_inter_distrib]
+        exact pi_inter_image (Set.disjoint_singleton_right.mpr t_fin)
+          (fun i hi ↦ hi ▸ (hC a ha).inter_mem (y a)
+          (hy1 a (Or.inl rfl)) (x a) (hx1 a (Or.inl rfl)))
+            <| IsSetSemiring.subset_disjointOfDiff h_ind' hx1' hy1'
+      have hG2 : PairwiseDisjoint G id := PairwiseDisjoint.image_of_le
+        (h_ind'.pairwiseDisjoint_disjointOfDiff hx1' hy1') <| fun _ _ hb ↦
+          Set.mem_of_mem_inter_right hb
+      have hG3 : ⋃₀ G = ((({a} : Set ι).pi x ∩ ({a} : Set ι).pi y)) ∩ (t.pi x \ t.pi y) := by
+        rw [← h_ind'.sUnion_disjointOfDiff hx1' hy1']
+        nth_rewrite 2 [sUnion_eq_iUnion]
+        rw [iUnion_coe_set, inter_iUnion₂, inter_comm]
+        simp only [mem_coe, sUnion_image, G]
+        rfl
+      use F.toFinset ∪ G.toFinset
+      simp only [coe_union, coe_toFinset]
+      refine ⟨union_subset_iff.mpr ⟨hF1, hG1⟩, ?_, ?_⟩
+      · apply (pairwiseDisjoint_union_of_disjoint (fun ⦃a b⦄ a ↦ a) hF2 hG2 )
+        rw [hF3, hG3]
+        nth_rewrite 2 [inter_comm]
+        exact h2
+      · rw [sUnion_union, hF3, hG3, h1]
+        nth_rewrite 2 [inter_comm]
+        rfl
+
+end piSemiring
+
 end IsSetSemiring
 
 /-- A ring of sets `C` is a family of sets containing `∅`, stable by union and set difference.
@@ -449,6 +629,7 @@ namespace IsSetRing
 lemma inter_mem (hC : IsSetRing C) (hs : s ∈ C) (ht : t ∈ C) : s ∩ t ∈ C := by
   rw [← diff_diff_right_self]; exact hC.diff_mem hs (hC.diff_mem hs ht)
 
+/-- A ring is a semi-ring. -/
 lemma isSetSemiring (hC : IsSetRing C) : IsSetSemiring C where
   empty_mem := hC.empty_mem
   inter_mem := fun _ hs _ ht => hC.inter_mem hs ht