-- Mathlib/Probability/Independence/Kernel.lean
theorem iIndepSet.iIndepFun_indicator [Zero β] [One β] {m : MeasurableSpace β} {s : ι → Set Ω}
    (hs : iIndepSet s κ μ) :
    iIndepFun (fun _n => m) (fun n => (s n).indicator fun _ω => 1) κ μ

Proof state:
case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 0 ∉ π i
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (generateFrom {s i})

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ,
        (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω => 1) ⁻¹' sets i) =
          ∏ i ∈ S, (κ a) (((s i).indicator fun _ω => 1) ⁻¹' sets i)

Tactic:
rintro S π _hπ

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω => 1) ⁻¹' π i) = ∏ i ∈ S, (κ a) (((s i).indicator fun _ω => 1) ⁻¹' π i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ iIndepFun (fun _n => m) (fun n => (s n).indicator fun _ω => 1) κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
⊢ ∀ (S : Finset ι) {sets : ι → Set β},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      ∀ᵐ (a : α) ∂μ,
        (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω => 1) ⁻¹' sets i) =
          ∏ i ∈ S, (κ a) (((s i).indicator fun _ω => 1) ⁻¹' sets i)

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, ((s i).indicator fun _ω => 1) ⁻¹' π i) = ∏ i ∈ S, (κ a) (((s i).indicator fun _ω => 1) ⁻¹' π i)

Tactic:
simp_rw [Set.indicator_const_preimage_eq_union]

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) =
      ∏ x ∈ S, (κ a) ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅)

Proof state:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 1 ∉ π i
⊢ MeasurableSet ∅

Tactic:
exact @MeasurableSet.empty _ (generateFrom {s i})

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
⊢ ∀ᵐ (a : α) ∂μ,
    (κ a) (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) =
      ∏ x ∈ S, (κ a) ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅)

Tactic:
refine @hs S (fun i => ite (1 ∈ π i) (s i) ∅ ∪ ite ((0 : β) ∈ π i) (s i)ᶜ ∅) fun i _hi => ?_

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ 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

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ 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

Tactic:
have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
  measurableSet_generateFrom (Set.mem_singleton _)

Result:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ 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

Proof state:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ 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

Tactic:
refine
  MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
    (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)

Result:
case refine_1
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 1 ∉ π i
⊢ MeasurableSet ∅

case refine_2
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
_mα : MeasurableSpace α
_mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst✝¹ : Zero β
inst✝ : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : ι → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
x✝ : 0 ∉ π i
⊢ MeasurableSet ∅