awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
ω : Ω
hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) ⋯ ω
⊢ Eq.{u_8 + 1} (α := β) (∏ c ∈ s, AEMeasurable.mk (f c) ⋯ ω) (∏ c ∈ s, f c ω)

Tactic:
Finset.prod_congr rfl fun i hi ↦ (hω ⟨i, hi⟩).symm

Premises used: Finset.prod_congr, Subtype.mk, Eq.symm, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
this :
  ∀ᵐ (a : α) ∂μ,
    ∀ (i : ↥s),
      f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
a : α
ha :
  ∀ (i : ↥s),
    f (↑i : ι) =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] AEMeasurable.mk (f (↑i : ι)) ⋯
ω : Ω
hω : ∀ (i : ↥s), f (↑i : ι) ω = AEMeasurable.mk (f (↑i : ι)) ⋯ ω
⊢ Eq.{u_8 + 1} (α := β) (∏ c ∈ s, AEMeasurable.mk (f c) ⋯ ω) (∏ c ∈ s, f c ω)

Tactic:
exact Finset.prod_congr rfl fun i hi ↦ (hω ⟨i, hi⟩).symm

Premises used: Finset.prod_congr, rfl
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i

Tactic:
Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk.symm

Premises used: Filter.EventuallyEq, MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ι → Ω → β
hf_Indep : iIndepFun (β := fun (x : ι) ↦ β) f κ μ
hf_meas : ∀ (i : ι), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
s : Finset ι
i : ι
hi : i ∉ s
h : IndepFun (β := β) (∏ j ∈ s, AEMeasurable.mk (f j) ⋯) (AEMeasurable.mk (f i) ⋯) κ μ
⊢ ∀ᵐ (a : α) ∂μ, AEMeasurable.mk (f i) ⋯ =ᶠ[ae (F := Measure Ω) ((κ : (a : α) → Measure Ω) a : Measure Ω)] f i

Tactic:
exact Measure.ae_ae_of_ae_comp (hf_meas i).ae_eq_mk.symm

Premises used: MeasureTheory.Measure.ae_ae_of_ae_comp, AEMeasurable.ae_eq_mk, Filter.EventuallyEq.symm
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ℕ → Ω → β
hf_Indep : iIndepFun (β := fun (x : ℕ) ↦ β) f κ μ
hf_meas : ∀ (i : ℕ), Measurable (f i)
n : ℕ
⊢ IndepFun (β := β) (∏ j ∈ Finset.range n, f j) (f n) κ μ

Tactic:
hf_Indep.indepFun_finsetProd_of_notMem hf_meas Finset.notMem_range_self

Premises used: Finset.notMem_range_self, ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
β : Type u_8
m : MeasurableSpace β
inst : CommMonoid β
inst_1 : MeasurableMul₂ β
f : ℕ → Ω → β
hf_Indep : iIndepFun (β := fun (x : ℕ) ↦ β) f κ μ
hf_meas : ∀ (i : ℕ), AEMeasurable (_m := mΩ) (f i) ((⇑κ : (a : α) → Measure Ω) ∘ₘ μ)
n : ℕ
⊢ IndepFun (β := β) (∏ j ∈ Finset.range n, f j) (f n) κ μ

Tactic:
hf_Indep.indepFun_finsetProd_of_notMem₀ hf_meas Finset.notMem_range_self

Premises used: Finset.notMem_range_self, ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem₀
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
rw :
  ∀ (S : Finset ι) {sets : (i : ι) → Set β} (_H : ∀ i ∈ S, MeasurableSet (sets i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
          ENNReal)
        (∏ i ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' sets i) :
          ENNReal)
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ

Tactic:
rw [iIndepFun_iff_measure_inter_preimage_eq_mul]

Premises used: ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
simp_rw :
  ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
        ENNReal)
      (∏ x ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
        ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
        ENNReal)
      (∏ i ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
        ENNReal)

Tactic:
simp_rw [Set.indicator_const_preimage_eq_union]

Premises used: Set.indicator_const_preimage_eq_union
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
apply :
  ∀ (i : ι) (_hi : i ∈ S),
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
      ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal)
      ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
          (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
        ENNReal)
      (∏ x ∈ S,
          (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
        ENNReal)

Tactic:
apply hs _ fun i _hi ↦ ?_
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
⊢ MeasurableSet (s i)

Tactic:
have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
⊢ Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)

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

Premises used: MeasurableSet, MeasurableSet.ite', Set.Mem, setOf, MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
refine_1 : 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
refine_2 : 0 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
⊢ Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
    ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)

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

Premises used: MeasurableSet.ite', MeasurableSet.compl, MeasurableSet.union
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
h : 1 ∉ π i
⊢ MeasurableSet.{u_2} (α := Ω) ∅

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

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
h : 1 ∉ π i
⊢ MeasurableSet.{u_2} (α := Ω) ∅

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

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
h : 0 ∉ π i
⊢ MeasurableSet.{u_2} (α := Ω) ∅

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

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
S : Finset ι
π : (i : ι) → Set β
_hπ : ∀ i ∈ S, MeasurableSet (π i)
i : ι
_hi : i ∈ S
hsi : MeasurableSet (s i)
h : 0 ∉ π i
⊢ MeasurableSet.{u_2} (α := Ω) ∅

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

Premises used: MeasurableSet.empty
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
inst : Zero β
inst_1 : One β
m : MeasurableSpace β
s : ι → Set Ω
hs : iIndepSet s κ μ
rw rw₁ rw₂ rw₃ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, ((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
        (∏ i ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              (((s i).indicator fun (_ω : Ω) ↦ 1) ⁻¹' π i) :
          ENNReal)
rw₄ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal)
        ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
            (⋂ i ∈ S, (if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅) :
          ENNReal)
        (∏ x ∈ S,
            (((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal)
              ((if 1 ∈ π x then s x else ∅) ∪ if 0 ∈ π x then (s x)ᶜ else ∅) :
          ENNReal)
rw₅ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S),
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
      ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
rw₆ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
    (hsi : MeasurableSet (s i)),
    Membership.mem (γ := Set (Set Ω)) ((fun (x : ι) ↦ ({s_1 : Set Ω | MeasurableSet s_1} : Set (Set Ω))) i)
      ((if 1 ∈ π i then s i else ∅) ∪ if 0 ∈ π i then (s i)ᶜ else ∅)
refine_1 :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
    (hsi : MeasurableSet (s i)), 1 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
refine_2 refine_2₁ :
  ∀ (S : Finset ι) {π : (i : ι) → Set β} (_hπ : ∀ i ∈ S, MeasurableSet (π i)) (i : ι) (_hi : i ∈ S)
    (hsi : MeasurableSet (s i)), 0 ∉ π i → MeasurableSet.{u_2} (α := Ω) ∅
⊢ iIndepFun (β := fun (n : ι) ↦ β) (fun (n : ι) ↦ (s n).indicator fun (_ω : Ω) ↦ 1) κ μ

Tactic:
classical
  rw [iIndepFun_iff_measure_inter_preimage_eq_mul]
  rintro S π _hπ
  simp_rw [Set.indicator_const_preimage_eq_union]
  apply hs _ fun i _hi ↦ ?_
  have hsi : MeasurableSet[generateFrom {s i}] (s i) :=
    measurableSet_generateFrom (Set.mem_singleton _)
  refine
    MeasurableSet.union (MeasurableSet.ite' (fun _ => hsi) fun _ => ?_)
      (MeasurableSet.ite' (fun _ => hsi.compl) fun _ => ?_)
  · exact @MeasurableSet.empty _ (generateFrom {s i})
  · exact @MeasurableSet.empty _ (generateFrom {s i})

Premises used: Set.indicator_const_preimage_eq_union, ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
intro :
  ∀ (val : Fintype ι),
    ∀ᵐ (a : α) ∂μ,
      Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
        (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)
⊢ ∀ᵐ (a : α) ∂μ,
    Eq (α := ENNReal) (((κ : (a : α) → Measure Ω) a)[⋂ i ∈ s, f i | ⋂ (i : ι), Y i ⁻¹' t i] : ENNReal)
      (∏ i ∈ s, ((κ : (a : α) → Measure Ω) a)[f i | Y i ⁻¹' t i] : ENNReal)

Tactic:
cases nonempty_fintype ι

Premises used: nonempty_fintype
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
h :
  ∀ (x : Ω),
    Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
      x ∈ Y i ⁻¹' t i
⊢ (fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i) = Y i ⁻¹' t i

Tactic:
ext
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
i : ι
x : Ω
⊢ Membership.mem (γ := Set Ω) ((fun (ω : Ω) ↦ (X i ω, Y i ω)) ⁻¹' SProd.sprod (α := Set α) univ (t i)) x ↔
    x ∈ Y i ⁻¹' t i

Tactic:
simp
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
⊢ ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)

Tactic:
have hYt i : MeasurableSet[(mα.prod mβ).comap fun ω ↦ (X i ω, Y i ω)] (Y i ⁻¹' t i) :=
    ⟨.univ ×ˢ t i, .prod .univ (ht _), by ext; simp⟩
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
pos : ∀ (hi : i ∈ s), MeasurableSet (g i)
neg : ∀ (hi : i ∉ s), MeasurableSet (g i)
⊢ MeasurableSet (g i)

Tactic:
by_cases hi : i ∈ s
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
pos : MeasurableSet (Y i ⁻¹' t i ∩ f i)
⊢ MeasurableSet (g i)

Tactic:
simp only [hi, ↓reduceIte, g]

Premises used: reduceIte
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∉ s
neg : MeasurableSet (Y i ⁻¹' t i)
⊢ MeasurableSet (g i)

Tactic:
simp only [hi, ↓reduceIte, g]

Premises used: reduceIte
-- Module: Mathlib.Probability.Independence.Kernel.IndepFun
Goal:
α : Type u_1
Ω : Type u_2
ι : Type u_3
β : Type u_4
mα : MeasurableSpace α
mΩ : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
mβ : MeasurableSpace β
X : ι → Ω → α
Y : ι → Ω → β
f : ι → Set Ω
t : ι → Set β
s : Finset ι
inst : Finite ι
hY : ∀ (i : ι), Measurable (Y i)
hindep : iIndepFun (β := fun (i : ι) ↦ α × β) (fun (i : ι) (ω : Ω) ↦ (X i ω, Y i ω)) κ μ
hf : ∀ i ∈ s, MeasurableSet (f i)
hy :
  ∀ᵐ (a : α) ∂μ,
    ∀ i ∉ s,
      Ne (α := ENNReal) ((((κ : (a : α) → Measure Ω) a : Measure Ω) : (a : Set Ω) → ENNReal) (Y i ⁻¹' t i) : ENNReal)
        (0 : ENNReal)
ht : ∀ (i : ι), MeasurableSet (t i)
val : Fintype ι
g : (i' : ι) → Set Ω := fun (i' : ι) ↦ if i' ∈ s then Y i' ⁻¹' t i' ∩ f i' else Y i' ⁻¹' t i'
hYt : ∀ (i : ι), MeasurableSet (Y i ⁻¹' t i)
i : ι
hi : i ∈ s
pos : ∀ (A : Set α) (hA : MeasurableSet A) (hA' : X i ⁻¹' A = f i), MeasurableSet (Y i ⁻¹' t i ∩ f i)
⊢ MeasurableSet (Y i ⁻¹' t i ∩ f i)

Tactic:
obtain ⟨A, hA, hA'⟩ := hf i hi