Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ (i : ι), i ∈ S → MeasurableSet (sets i)) →
      ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (Set.indicator (s i) fun _ω => 1) ⁻¹' sets i) =
        ∏ i in S, ↑↑μ ((Set.indicator (s i) fun _ω => 1) ⁻¹' sets i)
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
⊢ iIndepFun (fun _n => m) fun n => Set.indicator (s n) fun _ω => 1
rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
⊢ ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (Set.indicator (s i) fun _ω => 1) ⁻¹' π i) =
    ∏ i in S, ↑↑μ ((Set.indicator (s i) fun _ω => 1) ⁻¹' π i)
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ (i : ι), i ∈ S → MeasurableSet (sets i)) →
      ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (Set.indicator (s i) fun _ω => 1) ⁻¹' sets i) =
        ∏ i in S, ↑↑μ ((Set.indicator (s i) fun _ω => 1) ⁻¹' sets i)
rintro S π _hπ
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
⊢ ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) =
    ∏ x in S, ↑↑μ ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then s xᶜ else ∅)
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
⊢ ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (Set.indicator (s i) fun _ω => 1) ⁻¹' π i) =
    ∏ i in S, ↑↑μ ((Set.indicator (s i) fun _ω => 1) ⁻¹' π i)
simp_rw [Set.indicator_const_preimage_eq_union]
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
⊢ (fun i => (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) i ∈ (fun x => {s_1 | MeasurableSet s_1}) i
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
⊢ ↑↑μ (⋂ (i : ι) (_ : i ∈ S), (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) =
    ∏ x in S, ↑↑μ ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then s xᶜ else ∅)
refine' @hs S (fun i => ite (1 ∈ π i) (s i) ∅ ∪ ite ((0 : β) ∈ π i) (s iᶜ) ∅) fun i _hi => _
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
⊢ (fun i => (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) i ∈ (fun x => {s_1 | MeasurableSet s_1}) i
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
⊢ (fun i => (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) i ∈ (fun x => {s_1 | MeasurableSet s_1}) i
have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
  measurableSet_generateFrom (Set.mem_singleton _)
case refine'_1
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : ¬1 ∈ π i
⊢ MeasurableSet ∅

case refine'_2
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : ¬0 ∈ π i
⊢ MeasurableSet ∅
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
⊢ (fun i => (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then s iᶜ else ∅) i ∈ (fun x => {s_1 | MeasurableSet s_1}) i
refine'
  MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => _)
    (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => _)
no goals
case refine'_1
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : ¬1 ∈ π i
⊢ MeasurableSet ∅
exact @MeasurableSet.empty _ (generateFrom {s i})
no goals
case refine'_2
Ω : Type u_2
ι : Type u_3
β : Type u_1
β' : Type ?u.3674153
γ : Type ?u.3674156
γ' : Type ?u.3674159
mΩ : MeasurableSpace Ω
μ : MeasureTheory.Measure Ω
f : Ω → β
g : Ω → β'
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s
S : Finset ι
π : ι → Set β
_hπ : ∀ (i : ι), i ∈ S → MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : ¬0 ∈ π i
⊢ MeasurableSet ∅
exact @MeasurableSet.empty _ (generateFrom {s i})