Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ Indep (generateFrom (piiUnionInter (fun k => {s k}) S)) (generateFrom (piiUnionInter (fun k => {s k}) T))
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ Indep (generateFrom {t | ∃ n, n ∈ S ∧ s n = t}) (generateFrom {t | ∃ k, k ∈ T ∧ s k = t})
rw [← generateFrom_piiUnionInter_singleton_left, ← generateFrom_piiUnionInter_singleton_left]
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
t : Set Ω
ht : t ∈ piiUnionInter (fun k => {s k}) S
⊢ ∀ (n : ι), generateFrom {s n} ≤ m0

case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
t : Set Ω
ht : t ∈ piiUnionInter (fun k => {s k}) T
⊢ ∀ (n : ι), generateFrom {s n} ≤ m0

case refine'_3
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IsPiSystem (piiUnionInter (fun k => {s k}) S)

case refine'_4
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IsPiSystem (piiUnionInter (fun k => {s k}) T)

case refine'_5
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IndepSets (piiUnionInter (fun k => {s k}) S) (piiUnionInter (fun k => {s k}) T)
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ Indep (generateFrom (piiUnionInter (fun k => {s k}) S)) (generateFrom (piiUnionInter (fun k => {s k}) T))
refine'
  IndepSets.indep'
    (fun t ht => generateFrom_piiUnionInter_le _ _ _ _ (measurableSet_generateFrom ht))
    (fun t ht => generateFrom_piiUnionInter_le _ _ _ _ (measurableSet_generateFrom ht)) _ _ _
no goals
case refine'_1
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
t : Set Ω
ht : t ∈ piiUnionInter (fun k => {s k}) S
⊢ ∀ (n : ι), generateFrom {s n} ≤ m0
exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
no goals
case refine'_2
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
t : Set Ω
ht : t ∈ piiUnionInter (fun k => {s k}) T
⊢ ∀ (n : ι), generateFrom {s n} ≤ m0
exact fun k => generateFrom_le fun t ht => (Set.mem_singleton_iff.1 ht).symm ▸ hsm k
no goals
case refine'_3
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IsPiSystem (piiUnionInter (fun k => {s k}) S)
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
no goals
case refine'_4
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IsPiSystem (piiUnionInter (fun k => {s k}) T)
exact isPiSystem_piiUnionInter _ (fun k => IsPiSystem.singleton _) _
no goals
case refine'_5
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IndepSets (piiUnionInter (fun k => {s k}) S) (piiUnionInter (fun k => {s k}) T)
classical exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) hs) hST
no goals
case refine'_5
Ω : Type u_1
ι : Type u_2
m0 : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
inst✝ : IsProbabilityMeasure μ
s : ι → Set Ω
hsm : ∀ (n : ι), MeasurableSet (s n)
hs : iIndepSet s
S T : Set ι
hST : Disjoint S T
⊢ IndepSets (piiUnionInter (fun k => {s k}) S) (piiUnionInter (fun k => {s k}) T)
exact indepSets_piiUnionInter_of_disjoint (iIndep.iIndepSets (fun n => rfl) hs) hST