chore(probability/independence): simplify the definition of pi_Union_…

…Inter (#17043)

Due to the simplification, `sup_closed` is no longer useful. Since it was introduced for this application and is not used anywhere else, I removed it.

src/data/set/lattice.lean

@@ -1835,38 +1835,6 @@ inf_infi_nat_succ u
 
 end set
 
-section sup_closed
-
-/-- A set `s` is sup-closed if for all `x₁, x₂ ∈ s`, `x₁ ⊔ x₂ ∈ s`. -/
-def sup_closed [has_sup α] (s : set α) : Prop := ∀ x1 x2, x1 ∈ s → x2 ∈ s → x1 ⊔ x2 ∈ s
-
-lemma sup_closed_singleton [semilattice_sup α] (x : α) : sup_closed ({x} : set α) :=
-λ _ _ y1_mem y2_mem, by { rw set.mem_singleton_iff at *, rw [y1_mem, y2_mem, sup_idem], }
-
-lemma sup_closed.inter [semilattice_sup α] {s t : set α} (hs : sup_closed s)
-  (ht : sup_closed t) :
-  sup_closed (s ∩ t) :=
-begin
-  intros x y hx hy,
-  rw set.mem_inter_iff at hx hy ⊢,
-  exact ⟨hs x y hx.left hy.left, ht x y hx.right hy.right⟩,
-end
-
-lemma sup_closed_of_totally_ordered [semilattice_sup α] (s : set α)
-  (hs : ∀ x y : α, x ∈ s → y ∈ s → y ≤ x ∨ x ≤ y) :
-  sup_closed s :=
-begin
-  intros x y hxs hys,
-  cases hs x y hxs hys,
-  { rwa (sup_eq_left.mpr h), },
-  { rwa (sup_eq_right.mpr h), },
-end
-
-lemma sup_closed_of_linear_order [linear_order α] (s : set α) : sup_closed s :=
-sup_closed_of_totally_ordered s (λ x y hxs hys, le_total y x)
-
-end sup_closed
-
 open set
 
 variables [complete_lattice β]

src/measure_theory/pi_system.lean

@@ -43,10 +43,8 @@ import measure_theory.measurable_space_def
   represented as the intersection of a finite number of elements from these sets.
 
 * `pi_Union_Inter` defines a new π-system from a family of π-systems `π : ι → set (set α)` and a
-  set of finsets `S : set (finset α)`. `pi_Union_Inter π S` is the set of sets that can be written
-  as `⋂ x ∈ t, f x` for some `t ∈ S` and sets `f x ∈ π x`. If `S` is union-closed, then it is a
-  π-system. The π-systems used to prove Kolmogorov's 0-1 law will be defined using this mechanism
-  (TODO).
+  set of indices `S : set ι`. `pi_Union_Inter π S` is the set of sets that can be written
+  as `⋂ x ∈ t, f x` for some finset `t ∈ S` and sets `f x ∈ π x`.
 
 ## Implementation details
 
@@ -329,25 +327,25 @@ section Union_Inter
 
 /-! ### π-system generated by finite intersections of sets of a π-system family -/
 
-/-- From a set of finsets `S : set (finset ι)` and a family of sets of sets `π : ι → set (set α)`,
-define the set of sets that can be written as `⋂ x ∈ t, f x` for some `t ∈ S` and sets `f x ∈ π x`.
-
-If `S` is union-closed and `π` is a family of π-systems, then it is a π-system.
-The π-systems used to prove Kolmogorov's 0-1 law are of that form. -/
-def pi_Union_Inter {α ι} (π : ι → set (set α)) (S : set (finset ι)) : set (set α) :=
-{s : set α | ∃ (t : finset ι) (htS : t ∈ S) (f : ι → set α) (hf : ∀ x, x ∈ t → f x ∈ π x),
+/-- From a set of indices `S : set ι` and a family of sets of sets `π : ι → set (set α)`,
+define the set of sets that can be written as `⋂ x ∈ t, f x` for some finset `t ⊆ S` and sets
+`f x ∈ π x`. If `π` is a family of π-systems, then it is a π-system. -/
+def pi_Union_Inter {α ι} (π : ι → set (set α)) (S : set ι) : set (set α) :=
+{s : set α | ∃ (t : finset ι) (htS : ↑t ⊆ S) (f : ι → set α) (hf : ∀ x, x ∈ t → f x ∈ π x),
   s = ⋂ x ∈ t, f x}
 
 /-- If `S` is union-closed and `π` is a family of π-systems, then `pi_Union_Inter π S` is a
 π-system. -/
 lemma is_pi_system_pi_Union_Inter {α ι} (π : ι → set (set α))
-  (hpi : ∀ x, is_pi_system (π x)) (S : set (finset ι)) (h_sup : sup_closed S) :
+  (hpi : ∀ x, is_pi_system (π x)) (S : set ι) :
   is_pi_system (pi_Union_Inter π S) :=
 begin
   rintros t1 ⟨p1, hp1S, f1, hf1m, ht1_eq⟩ t2 ⟨p2, hp2S, f2, hf2m, ht2_eq⟩ h_nonempty,
   simp_rw [pi_Union_Inter, set.mem_set_of_eq],
   let g := λ n, (ite (n ∈ p1) (f1 n) set.univ) ∩ (ite (n ∈ p2) (f2 n) set.univ),
-  use [p1 ∪ p2, h_sup p1 p2 hp1S hp2S, g],
+  have hp_union_ss : ↑(p1 ∪ p2) ⊆ S,
+  { simp only [hp1S, hp2S, finset.coe_union, union_subset_iff, and_self], },
+  use [p1 ∪ p2, hp_union_ss, g],
   have h_inter_eq : t1 ∩ t2 = ⋂ i ∈ p1 ∪ p2, g i,
   { rw [ht1_eq, ht2_eq],
     simp_rw [← set.inf_eq_inter, g],
@@ -380,15 +378,15 @@ begin
 end
 
 lemma pi_Union_Inter_mono_left {α ι} {π π' : ι → set (set α)} (h_le : ∀ i, π i ⊆ π' i)
-  (S : set (finset ι)) :
+  (S : set ι) :
   pi_Union_Inter π S ⊆ pi_Union_Inter π' S :=
 begin
   rintros s ⟨t, ht_mem, ft, hft_mem_pi, rfl⟩,
   exact ⟨t, ht_mem, ft, λ x hxt, h_le x (hft_mem_pi x hxt), rfl⟩,
 end
 
 lemma generate_from_pi_Union_Inter_le {α ι} {m : measurable_space α}
-  (π : ι → set (set α)) (h : ∀ n, generate_from (π n) ≤ m) (S : set (finset ι)) :
+  (π : ι → set (set α)) (h : ∀ n, generate_from (π n) ≤ m) (S : set ι) :
   generate_from (pi_Union_Inter π S) ≤ m :=
 begin
   refine generate_from_le _,
@@ -397,79 +395,47 @@ begin
   exact measurable_set_generate_from (hft_mem_pi x hx_mem),
 end
 
-lemma subset_pi_Union_Inter {α ι} {π : ι → set (set α)} {S : set (finset ι)}
-  (h_univ : ∀ i, set.univ ∈ π i) {i : ι} {s : finset ι} (hsS : s ∈ S) (his : i ∈ s) :
+lemma subset_pi_Union_Inter {α ι} {π : ι → set (set α)} {S : set ι} {i : ι} (his : i ∈ S) :
   π i ⊆ pi_Union_Inter π S :=
 begin
-  refine λ t ht_pii, ⟨s, hsS, (λ j, ite (j = i) t set.univ), ⟨λ m h_pm, _, _⟩⟩,
-  { split_ifs,
-    { rwa h, },
-    { exact h_univ m, }, },
-  { ext1 x,
-    simp_rw set.mem_Inter,
-    split; intro hx,
-    { intros j h_p_j,
-      split_ifs,
-      { exact hx, },
-      { exact set.mem_univ _, }, },
-    { simpa using hx i his, }, },
+  refine λ t ht_pii, ⟨{i}, _, (λ j, t), ⟨λ m h_pm, _, _⟩⟩,
+  { simp only [his, finset.coe_singleton, singleton_subset_iff], },
+  { rw finset.mem_singleton at h_pm,
+    rwa h_pm, },
+  { simp only [finset.mem_singleton, Inter_Inter_eq_left], },
 end
 
 lemma mem_pi_Union_Inter_of_measurable_set {α ι} (m : ι → measurable_space α)
-  {S : set (finset ι)} {i : ι} {t : finset ι} (htS : t ∈ S) (hit : i ∈ t) (s : set α)
+  {S : set ι} {i : ι} (hiS : i ∈ S) (s : set α)
   (hs : measurable_set[m i] s) :
   s ∈ pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S :=
-subset_pi_Union_Inter (λ i, measurable_set.univ) htS hit hs
+subset_pi_Union_Inter hiS hs
 
 lemma le_generate_from_pi_Union_Inter {α ι} {π : ι → set (set α)}
-  (S : set (finset ι)) (h_univ : ∀ n, set.univ ∈ π n) {x : ι}
-  {t : finset ι} (htS : t ∈ S) (hxt : x ∈ t) :
+  (S : set ι) {x : ι} (hxS : x ∈ S) :
   generate_from (π x) ≤ generate_from (pi_Union_Inter π S) :=
-generate_from_mono (subset_pi_Union_Inter h_univ htS hxt)
+generate_from_mono (subset_pi_Union_Inter hxS)
 
 lemma measurable_set_supr_of_mem_pi_Union_Inter {α ι} (m : ι → measurable_space α)
-  (S : set (finset ι)) (t : set α) (ht : t ∈ pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S) :
-  measurable_set[⨆ i (hi : ∃ s ∈ S, i ∈ s), m i] t :=
+  (S : set ι) (t : set α) (ht : t ∈ pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S) :
+  measurable_set[⨆ i ∈ S, m i] t :=
 begin
   rcases ht with ⟨pt, hpt, ft, ht_m, rfl⟩,
   refine pt.measurable_set_bInter (λ i hi, _),
-  suffices h_le : m i ≤ (⨆ i (hi : ∃ s ∈ S, i ∈ s), m i), from h_le (ft i) (ht_m i hi),
-  have hi' : ∃ s ∈ S, i ∈ s, from ⟨pt, hpt, hi⟩,
+  suffices h_le : m i ≤ (⨆ i ∈ S, m i), from h_le (ft i) (ht_m i hi),
+  have hi' : i ∈ S := hpt hi,
   exact le_supr₂ i hi',
 end
 
-lemma generate_from_pi_Union_Inter_measurable_space {α ι} (m : ι → measurable_space α)
-  (S : set (finset ι)) :
-  generate_from (pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S)
-    = ⨆ i (hi : ∃ p ∈ S, i ∈ p), m i :=
+lemma generate_from_pi_Union_Inter_measurable_set {α ι} (m : ι → measurable_space α) (S : set ι) :
+  generate_from (pi_Union_Inter (λ n, {s | measurable_set[m n] s}) S) = ⨆ i ∈ S, m i :=
 begin
   refine le_antisymm _ _,
-  { rw ← @generate_from_measurable_set α (⨆ i (hi : ∃ p ∈ S, i ∈ p), m i),
+  { rw ← @generate_from_measurable_set α (⨆ i ∈ S, m i),
     exact generate_from_mono (measurable_set_supr_of_mem_pi_Union_Inter m S), },
   { refine supr₂_le (λ i hi, _),
-    rcases hi with ⟨p, hpS, hpi⟩,
     rw ← @generate_from_measurable_set α (m i),
-    exact generate_from_mono (mem_pi_Union_Inter_of_measurable_set m hpS hpi), },
-end
-
-lemma generate_from_pi_Union_Inter_subsets {α ι} (m : ι → measurable_space α) (S : set ι) :
-  generate_from (pi_Union_Inter (λ i, {t | measurable_set[m i] t}) {t : finset ι | ↑t ⊆ S})
-    = ⨆ i ∈ S, m i :=
-begin
-  rw generate_from_pi_Union_Inter_measurable_space,
-  simp only [set.mem_set_of_eq, exists_prop, supr_exists],
-  congr' 1,
-  ext1 i,
-  by_cases hiS : i ∈ S,
-  { simp only [hiS, csupr_pos],
-    refine le_antisymm (supr₂_le (λ t ht, le_rfl)) _,
-    rw le_supr_iff,
-    intros m' hm',
-    specialize hm' {i},
-    simpa only [hiS, finset.coe_singleton, set.singleton_subset_iff, finset.mem_singleton,
-      eq_self_iff_true, and_self, csupr_pos] using hm', },
-  { simp only [hiS, supr_false, supr₂_eq_bot, and_imp],
-    exact λ t htS hit, absurd (htS hit) hiS, },
+    exact generate_from_mono (mem_pi_Union_Inter_of_measurable_set m hi), },
 end
 
 end Union_Inter

src/probability/independence.lean

@@ -348,22 +348,23 @@ end
 
 variables {m0 : measurable_space Ω} {μ : measure Ω}
 
-lemma indep_sets_pi_Union_Inter_of_disjoint [decidable_eq ι] [is_probability_measure μ]
-  {s : ι → set (set Ω)} {S T : set (finset ι)}
-  (h_indep : Indep_sets s μ) (hST : ∀ u v, u ∈ S → v ∈ T → disjoint u v) :
+lemma indep_sets_pi_Union_Inter_of_disjoint [is_probability_measure μ]
+  {s : ι → set (set Ω)} {S T : set ι}
+  (h_indep : Indep_sets s μ) (hST : disjoint S T) :
   indep_sets (pi_Union_Inter s S) (pi_Union_Inter s T) μ :=
 begin
   rintros t1 t2 ⟨p1, hp1, f1, ht1_m, ht1_eq⟩ ⟨p2, hp2, f2, ht2_m, ht2_eq⟩,
+  classical,
   let g := λ i, ite (i ∈ p1) (f1 i) set.univ ∩ ite (i ∈ p2) (f2 i) set.univ,
   have h_P_inter : μ (t1 ∩ t2) = ∏ n in p1 ∪ p2, μ (g n),
   { have hgm : ∀ i ∈ p1 ∪ p2, g i ∈ s i,
     { intros i hi_mem_union,
       rw finset.mem_union at hi_mem_union,
       cases hi_mem_union with hi1 hi2,
-      { have hi2 : i ∉ p2 := finset.disjoint_left.mp (hST p1 p2 hp1 hp2) hi1,
+      { have hi2 : i ∉ p2 := λ hip2, set.disjoint_left.mp hST (hp1 hi1) (hp2 hip2),
         simp_rw [g, if_pos hi1, if_neg hi2, set.inter_univ],
         exact ht1_m i hi1, },
-      { have hi1 : i ∉ p1 := finset.disjoint_right.mp (hST p1 p2 hp1 hp2) hi2,
+      { have hi1 : i ∉ p1 := λ hip1, set.disjoint_right.mp hST (hp2 hi2) (hp1 hip1),
         simp_rw [g, if_neg hi1, if_pos hi2, set.univ_inter],
         exact ht2_m i hi2, }, },
     have h_p1_inter_p2 : ((⋂ x ∈ p1, f1 x) ∩ ⋂ x ∈ p2, f2 x)
@@ -377,7 +378,7 @@ begin
   { intro n,
     simp_rw g,
     split_ifs,
-    { exact absurd rfl (finset.disjoint_iff_ne.mp (hST p1 p2 hp1 hp2) n h n h_1), },
+    { exact absurd rfl (set.disjoint_iff_forall_ne.mp hST _ (hp1 h) _ (hp2 h_1)), },
     all_goals { simp only [measure_univ, one_mul, mul_one, set.inter_univ, set.univ_inter], }, },
   simp_rw [h_P_inter, h_μg, finset.prod_mul_distrib,
     finset.prod_ite_mem (p1 ∪ p2) p1 (λ x, μ (f1 x)),
@@ -390,20 +391,12 @@ lemma indep_supr_of_disjoint [is_probability_measure μ] {m : ι → measurable_
   indep (⨆ i ∈ S, m i) (⨆ i ∈ T, m i) μ :=
 begin
   refine indep_sets.indep (supr₂_le (λ i _, h_le i)) (supr₂_le (λ i _, h_le i)) _ _
-    (generate_from_pi_Union_Inter_subsets m S).symm
-    (generate_from_pi_Union_Inter_subsets m T).symm _,
-  { refine is_pi_system_pi_Union_Inter _ (λ n, @is_pi_system_measurable_set Ω (m n)) _ _,
-    intros s t hs ht,
-    simp only [finset.sup_eq_union, set.mem_set_of_eq, finset.coe_union, set.union_subset_iff],
-    exact ⟨hs, ht⟩, },
-  { refine is_pi_system_pi_Union_Inter _ (λ n, @is_pi_system_measurable_set Ω (m n)) _ _,
-    intros s t hs ht,
-    simp only [finset.sup_eq_union, set.mem_set_of_eq, finset.coe_union, set.union_subset_iff],
-    exact ⟨hs, ht⟩, },
+    (generate_from_pi_Union_Inter_measurable_set m S).symm
+    (generate_from_pi_Union_Inter_measurable_set m T).symm _,
+  { exact is_pi_system_pi_Union_Inter _ (λ n, @is_pi_system_measurable_set Ω (m n)) _, },
+  { exact is_pi_system_pi_Union_Inter _ (λ n, @is_pi_system_measurable_set Ω (m n)) _ , },
   { classical,
-    refine indep_sets_pi_Union_Inter_of_disjoint h_indep (λ s t hs ht, _),
-    rw finset.disjoint_iff_ne,
-    exact λ i his j hjt, set.disjoint_iff_forall_ne.mp hST i (hs his) j (ht hjt), },
+    exact indep_sets_pi_Union_Inter_of_disjoint h_indep hST, },
 end
 
 lemma indep_supr_of_directed_le {Ω} {m : ι → measurable_space Ω}
@@ -444,19 +437,18 @@ indep_supr_of_directed_le h_indep h_le h_le' (directed_of_inf hm)
 
 lemma Indep_sets.pi_Union_Inter_singleton {π : ι → set (set Ω)} {a : ι} {S : finset ι}
   (hp_ind : Indep_sets π μ) (haS : a ∉ S) :
-  indep_sets (pi_Union_Inter π {S}) (π a) μ :=
+  indep_sets (pi_Union_Inter π S) (π a) μ :=
 begin
   rintros t1 t2 ⟨s, hs_mem, ft1, hft1_mem, ht1_eq⟩ ht2_mem_pia,
-  rw set.mem_singleton_iff at hs_mem,
-  subst hs_mem,
+  rw [finset.coe_subset] at hs_mem,
   classical,
   let f := λ n, ite (n = a) t2 (ite (n ∈ s) (ft1 n) set.univ),
   have h_f_mem : ∀ n ∈ insert a s, f n ∈ π n,
   { intros n hn_mem_insert,
     simp_rw f,
     cases (finset.mem_insert.mp hn_mem_insert) with hn_mem hn_mem,
     { simp [hn_mem, ht2_mem_pia], },
-    { have hn_ne_a : n ≠ a, by { rintro rfl, exact haS hn_mem, },
+    { have hn_ne_a : n ≠ a, by { rintro rfl, exact haS (hs_mem hn_mem), },
       simp [hn_ne_a, hn_mem, hft1_mem n hn_mem], }, },
   have h_f_mem_pi : ∀ n ∈ s, f n ∈ π n, from λ x hxS, h_f_mem x (by simp [hxS]),
   have h_t1 : t1 = ⋂ n ∈ s, f n,
@@ -466,96 +458,48 @@ begin
       congr' with hns y,
       simp only [(h_forall n hns).symm], },
     intros n hnS,
-    have hn_ne_a : n ≠ a, by { rintro rfl, exact haS hnS, },
+    have hn_ne_a : n ≠ a, by { rintro rfl, exact haS (hs_mem hnS), },
     simp_rw [f, if_pos hnS, if_neg hn_ne_a], },
   have h_μ_t1 : μ t1 = ∏ n in s, μ (f n), by rw [h_t1, ← hp_ind s h_f_mem_pi],
   have h_t2 : t2 = f a, by { simp_rw [f], simp, },
   have h_μ_inter : μ (t1 ∩ t2) = ∏ n in insert a s, μ (f n),
   { have h_t1_inter_t2 : t1 ∩ t2 = ⋂ n ∈ insert a s, f n,
       by rw [h_t1, h_t2, finset.set_bInter_insert, set.inter_comm],
     rw [h_t1_inter_t2, ← hp_ind (insert a s) h_f_mem], },
-  rw [h_μ_inter, finset.prod_insert haS, h_t2, mul_comm, h_μ_t1],
+  have has : a ∉ s := λ has_mem, haS (hs_mem has_mem),
+  rw [h_μ_inter, finset.prod_insert has, h_t2, mul_comm, h_μ_t1],
 end
 
-/-- Auxiliary lemma for `Indep_sets.Indep`. -/
-theorem Indep_sets.Indep_aux [is_probability_measure μ] (m : ι → measurable_space Ω)
+/-- The measurable space structures generated by independent pi-systems are independent. -/
+theorem Indep_sets.Indep [is_probability_measure μ] (m : ι → measurable_space Ω)
   (h_le : ∀ i, m i ≤ m0) (π : ι → set (set Ω)) (h_pi : ∀ n, is_pi_system (π n))
-  (hp_univ : ∀ i, set.univ ∈ π i) (h_generate : ∀ i, m i = generate_from (π i))
-  (h_ind : Indep_sets π μ) :
+  (h_generate : ∀ i, m i = generate_from (π i)) (h_ind : Indep_sets π μ) :
   Indep m μ :=
 begin
   classical,
-  refine finset.induction (by simp [measure_univ]) _,
+  refine finset.induction _ _,
+  { simp only [measure_univ, implies_true_iff, set.Inter_false, set.Inter_univ, finset.prod_empty,
+      eq_self_iff_true], },
   intros a S ha_notin_S h_rec f hf_m,
   have hf_m_S : ∀ x ∈ S, measurable_set[m x] (f x) := λ x hx, hf_m x (by simp [hx]),
   rw [finset.set_bInter_insert, finset.prod_insert ha_notin_S, ← h_rec hf_m_S],
-  let p := pi_Union_Inter π {S},
+  let p := pi_Union_Inter π S,
   set m_p := generate_from p with hS_eq_generate,
   have h_indep : indep m_p (m a) μ,
-  { have hp : is_pi_system p := is_pi_system_pi_Union_Inter π h_pi {S} (sup_closed_singleton S),
+  { have hp : is_pi_system p := is_pi_system_pi_Union_Inter π h_pi S,
     have h_le' : ∀ i, generate_from (π i) ≤ m0 := λ i, (h_generate i).symm.trans_le (h_le i),
-    have hm_p : m_p ≤ m0 := generate_from_pi_Union_Inter_le π h_le' {S},
+    have hm_p : m_p ≤ m0 := generate_from_pi_Union_Inter_le π h_le' S,
     exact indep_sets.indep hm_p (h_le a) hp (h_pi a) hS_eq_generate (h_generate a)
       (h_ind.pi_Union_Inter_singleton ha_notin_S), },
   refine h_indep.symm (f a) (⋂ n ∈ S, f n) (hf_m a (finset.mem_insert_self a S)) _,
   have h_le_p : ∀ i ∈ S, m i ≤ m_p,
   { intros n hn,
     rw [hS_eq_generate, h_generate n],
-    exact le_generate_from_pi_Union_Inter {S} hp_univ (set.mem_singleton _) hn, },
+    exact le_generate_from_pi_Union_Inter S hn, },
   have h_S_f : ∀ i ∈ S, measurable_set[m_p] (f i) := λ i hi, (h_le_p i hi) (f i) (hf_m_S i hi),
   exact S.measurable_set_bInter h_S_f,
 end
 
-/-- The measurable space structures generated by independent pi-systems are independent. -/
-theorem Indep_sets.Indep [is_probability_measure μ] (m : ι → measurable_space Ω)
-  (h_le : ∀ i, m i ≤ m0) (π : ι → set (set Ω)) (h_pi : ∀ n, is_pi_system (π n))
-  (h_generate : ∀ i, m i = generate_from (π i)) (h_ind : Indep_sets π μ) :
-  Indep m μ :=
-begin
-  -- We want to apply `Indep_sets.Indep_aux`, but `π i` does not contain `univ`, hence we replace
-  -- `π` with a new augmented pi-system `π'`, and prove all hypotheses for that pi-system.
-  let π' := λ i, insert set.univ (π i),
-  have h_subset : ∀ i, π i ⊆ π' i := λ i, set.subset_insert _ _,
-  have h_pi' : ∀ n, is_pi_system (π' n) := λ n, (h_pi n).insert_univ,
-  have h_univ' : ∀ i, set.univ ∈ π' i, from λ i, set.mem_insert _ _,
-  have h_gen' : ∀ i, m i = generate_from (π' i),
-  { intros i,
-    rw [h_generate i, generate_from_insert_univ (π i)], },
-  have h_ind' : Indep_sets π' μ,
-  { intros S f hfπ',
-    classical,
-    let S' := finset.filter (λ i, f i ≠ set.univ) S,
-    have h_mem : ∀ i ∈ S', f i ∈ π i,
-    { intros i hi,
-      simp_rw [S', finset.mem_filter] at hi,
-      cases hfπ' i hi.1,
-      { exact absurd h hi.2, },
-      { exact h, }, },
-    have h_left : (⋂ i ∈ S, f i) = ⋂ i ∈ S', f i,
-    { ext1 x,
-      simp only [set.mem_Inter, finset.mem_filter, ne.def, and_imp],
-      split,
-      { exact λ h i hiS hif, h i hiS, },
-      { intros h i hiS,
-        by_cases hfi_univ : f i = set.univ,
-        { rw hfi_univ, exact set.mem_univ _, },
-        { exact h i hiS hfi_univ, }, }, },
-    have h_right : ∏ i in S, μ (f i) = ∏ i in S', μ (f i),
-    { rw ← finset.prod_filter_mul_prod_filter_not S (λ i, f i ≠ set.univ),
-      simp only [ne.def, finset.filter_congr_decidable, not_not],
-      suffices : ∏ x in finset.filter (λ x, f x = set.univ) S, μ (f x) = 1,
-      { rw [this, mul_one], },
-      calc ∏ x in finset.filter (λ x, f x = set.univ) S, μ (f x)
-          = ∏ x in finset.filter (λ x, f x = set.univ) S, μ set.univ :
-            finset.prod_congr rfl (λ x hx, by { rw finset.mem_filter at hx, rw hx.2, })
-      ... = ∏ x in finset.filter (λ x, f x = set.univ) S, 1 :
-            finset.prod_congr rfl (λ _ _, measure_univ)
-      ... = 1 : finset.prod_const_one, },
-    rw [h_left, h_right],
-    exact h_ind S' h_mem, },
-  exact Indep_sets.Indep_aux m h_le π' h_pi' h_univ' h_gen' h_ind',
-end
-
 end from_pi_systems_to_measurable_spaces
 
 section indep_set