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
+  apply pairwiseDisjoint_union.mpr ⟨hs, ht, ?_⟩
+  exact fun a ha b hb hab ↦ Disjoint.mono (hf (subset_sUnion_of_subset s a (subset_refl a) ha))
+      (hf (subset_sUnion_of_subset t b (subset_refl b) hb)) hst
+
 end PartialOrderBot
 
 section CompleteLattice

Mathlib/Data/Set/Prod.lean

@@ -730,6 +730,23 @@ 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
+  have hx : ∀ i ∈ s, x i = if h : i ∈ s then x i else y i := by
+    intro i hi
+    simp only [dite_eq_ite, hi, ↓reduceIte]
+  have hy : ∀ i ∈ t, y i = if h : i ∈ s then x i else y i := by
+    intro i hi
+    have h : i ∉ s := Disjoint.not_mem_of_mem_left (id (Disjoint.symm hst)) hi
+    simp only [hi, hst, dite_eq_ite, h, ↓reduceIte]
+  rw [Set.pi_congr rfl hx, Set.pi_congr rfl hy]
+  exact union_pi
+
 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
@@ -890,6 +907,58 @@ 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 \ t.pi y) ∩ (s.pi x ∩ s.pi y) ∪
+    t.pi x ∩ (s.pi x \ s.pi y) := by
+    ext z
+    refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+    · simp only [mem_diff, mem_inter_iff, Set.mem_preimage, Function.eval, Set.mem_pi, not_and,
+          not_forall, Classical.not_imp] at h
+      obtain ⟨h1, ⟨j, ⟨hj1, hj2⟩⟩⟩ := h
+      by_cases hz : ∃ a ∈ s, z a ∉ y a
+      · right
+        simp only [mem_inter_iff, Set.mem_pi, mem_diff, not_forall, Classical.not_imp]
+        refine ⟨fun i hi ↦ h1 i (Set.subset_union_right hi),
+          fun i hi ↦ h1 i (Set.subset_union_left hi), bex_def.mpr hz⟩
+      · simp only [not_exists, not_and, not_not] at hz
+        left
+        simp only [mem_inter_iff, mem_diff, Set.mem_pi, not_forall, Classical.not_imp,
+          Set.mem_preimage, Function.eval]
+        refine ⟨⟨fun i hi ↦ h1 i (Set.subset_union_right hi), ?_⟩,
+          fun i hi ↦ h1 i (Set.subset_union_left hi), hz⟩
+        · have hj : j ∈ t := by
+            simp only [Set.mem_union] at hj1
+            rcases hj1 with (g1 | g2)
+            · exact False.elim (hj2 (hz j g1))
+            · exact g2
+          exact ⟨j, hj, hj2⟩
+    · simp only [Set.mem_union, mem_inter_iff, mem_diff, Set.mem_pi, not_forall,
+      Classical.not_imp] at h
+      simp only [mem_diff, Set.mem_pi, Set.mem_union, not_forall, Classical.not_imp]
+      rcases h with ⟨⟨h11, h12⟩, h2, h3⟩ | ⟨h1, h2, h3⟩
+      · refine ⟨?_, ?_⟩
+        · rintro i (hi1 | hi2)
+          · exact h2 i hi1
+          · exact h11 i hi2
+        · obtain ⟨x, hx1, hx2⟩ := h12
+          exact ⟨x, Or.inr hx1, hx2⟩
+      · refine ⟨?_, ?_⟩
+        · rintro i (hi1 | hi2)
+          · exact h2 i hi1
+          · exact h1 i hi2
+        · obtain ⟨x, hx1, hx2⟩ := h3
+          exact ⟨x, Or.inl hx1, hx2⟩
+
+lemma pi_setdiff_union_disjoint (s t : Set ι) (x : (i : ι) → Set (α i)) (y : (i : ι) → Set (α i)) :
+  Disjoint ((t.pi x \ t.pi y) ∩ (s.pi x ∩ s.pi y)) (t.pi x ∩ (s.pi x \ s.pi y)) :=
+  Disjoint.mono (inter_subset_right) (inter_subset_right) <|
+    Disjoint.mono Set.inter_subset_right (fun ⦃_⦄ a ↦ a) <| disjoint_sdiff_right
+
+end Setdiff
+
 end Pi
 
 end Set
@@ -927,3 +996,18 @@ theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t :
   · rintro ⟨h₁, h₂⟩ (i|i) <;> simp <;> apply_assumption
 
 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

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 α] :