awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
x : Ω
x_1 : ι
x_2 : κ x_1
⊢ Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      (fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω) x x_1
      x_2 =
    X x_1 x_2 x

Tactic:
simp [Sigma.curry]

Premises used: Sigma.curry
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
⊢ Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω

Tactic:
have : (MeasurableEquiv.piCurry 𝓧) ∘ (fun ω p ↦ X p.1 p.2 ω) = fun ω i j ↦ X i j ω := by
    ext; simp [Sigma.curry]
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
⊢ ∀ (i : (i : ι) × κ i),
    Measurable.{u_2, u_5} (β := 𝓧 (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) fun (ω : Ω) ↦
      X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) ω

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
⊢ Measurable (α := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))) (β :=
    (i : ι) → (j : κ i) → 𝓧 i j)
    (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
⊢ Measurable (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    fun (ω : Ω) (i : (i : ι) × κ i) ↦ X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) ω

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
⊢ ∀ (i : ι), Measurable (β := (x : κ i) → 𝓧 i x) fun (ω : Ω) (x : κ i) ↦ X i x ω

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
rw :
  Eq (α := Measure ((i : ι) → (j : κ i) → 𝓧 i j))
    (infinitePi (X := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) fun (i : ι) ↦ map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → 𝓧 i i_1) fun (i : ι) ↦
      infinitePi (X := 𝓧 i) fun (j : κ i) ↦ map (X i j) P)
⊢ iIndepFun (β := fun (p : (i : ι) × κ i) ↦ 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (fun (p : (i : ι) × κ i) (ω : Ω) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω) P

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop),
    ← (MeasurableEquiv.piCurry 𝓧).map_measurableEquiv_injective.eq_iff,
    map_map (by fun_prop) (by fun_prop), this,
    (iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)).1 h1,
    infinitePi_map_piCurry (fun i j ↦ P.map (X i j))]

Premises used: MeasureTheory.Measure.infinitePi_map_piCurry, Function.Injective.eq_iff, MeasureTheory.Measure.map, Iff.mp, MeasurableEquiv.piCurry, MeasurableEquiv.map_measurableEquiv_injective, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
congrm :
  ∀ (i : ι),
    Eq (α := Measure ((x : κ i) → 𝓧 i x)) (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
      (infinitePi (X := 𝓧 i) fun (j : κ i) ↦ map (X i j) P)
⊢ Eq (α := Measure ((i : ι) → (j : κ i) → 𝓧 i j))
    (infinitePi (X := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) fun (i : ι) ↦ map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → 𝓧 i i_1) fun (i : ι) ↦
      infinitePi (X := 𝓧 i) fun (j : κ i) ↦ map (X i j) P)

Tactic:
congrm infinitePi fun i ↦ ?_

Premises used: MeasureTheory.Measure.infinitePi
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
i : ι
⊢ ∀ (i_1 : κ i), Measurable (X i i_1)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ i) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ i) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
this_1 : IsProbabilityMeasure P
this_2 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
this_3 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
this :
  Eq (α := Ω → (i : ι) → (j : κ i) → 𝓧 i j)
    (Function.comp (β := (p : (i : ι) × κ i) → 𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(MeasurableEquiv.piCurry (κ := κ) 𝓧) : (a : (p : (i : ι) × κ i) → 𝓧 p.fst p.snd) → (i : ι) → (j : κ i) → 𝓧 i j)
      fun (ω : Ω) (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)) ω)
    fun (ω : Ω) (i : ι) (j : κ i) ↦ X i j ω
i : ι
rw rw₁ :
  Eq (α := Measure ((x : κ i) → 𝓧 i x)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) P)
    (infinitePi (X := 𝓧 i) fun (j : κ i) ↦ map (X i j) P)
⊢ Eq (α := Measure ((x : κ i) → 𝓧 i x)) (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
    (infinitePi (X := 𝓧 i) fun (j : κ i) ↦ map (X i j) P)

Tactic:
rw [(iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)).1 (h2 i)]

Premises used: Iff.mp, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ ∀ (i : ι) (j : κ i),
    Measurable (α := (i : ι) → (i_1 : κ i) → Ω i i_1) (β := 𝓧 i j)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i j)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
refine_1 :
  iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := fun (i : ι) ↦
    (x : κ i) → 𝓧 i x)
    (fun (i : ι) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (x : κ i) ↦
      (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i x ω)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
refine_2 :
  ∀ (i : ι),
    iIndepFun (Ω := (i : ι) → (i_1 : κ i) → Ω i i_1) (_mΩ :=
      MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := 𝓧 i)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))
⊢ iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (j : κ i) → Ω i j)) (β := fun (p : (i : ι) × κ i) ↦
    𝓧 (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (fun (p : (i : ι) × κ i) (ω : (i : ι) → (j : κ i) → Ω i j) ↦
      X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))
        (ω (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (i : ι) ↦ (j : κ i) → Ω i j) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))

Tactic:
refine iIndepFun_uncurry (P := infinitePi (fun i ↦ infinitePi (μ i)))
    (X := fun i j ω ↦ X i j (ω i j)) (by fun_prop) ?_ fun i ↦ ?_

Premises used: ProbabilityTheory.iIndepFun_uncurry
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ ∀ (i : ι),
    Measurable (α := (i_1 : κ i) → Ω i i_1) (β := (j : κ i) → 𝓧 i j)
      ((fun (i : ι) (u : (i_1 : κ i) → Ω i i_1) (j : κ i) ↦ X i j (u j)) i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
⊢ iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := fun (i : ι) ↦
    (x : κ i) → 𝓧 i x)
    (fun (i : ι) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (x : κ i) ↦
      (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i x ω)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))

Tactic:
exact iIndepFun_infinitePi (P := fun i ↦ infinitePi (μ i))
      (X := fun i u j ↦ X i j (u j)) (by fun_prop)

Premises used: ProbabilityTheory.iIndepFun_infinitePi
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ ∀ (i_1 : κ i),
    Measurable (α := (i : ι) → (i_2 : κ i) → Ω i i_2) (β := 𝓧 i i_1)
      ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((i_1 : κ i) → 𝓧 i i_1))
    (map
      (fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i_1 : κ i) ↦
        (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1 ω)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
⊢ iIndepFun (Ω := (i : ι) → (i_1 : κ i) → Ω i i_1) (_mΩ :=
    MeasurableSpace.pi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1)) (β := 𝓧 i)
    ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) ↦ X i j (ω i j)) i)
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)]

Premises used: ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
⊢ Eq (α := Measure ((i_1 : κ i) → 𝓧 i i_1))
    (map
      (fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i_1 : κ i) ↦
        (fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1 ω)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))

Tactic:
change map ((fun f ↦ f i) ∘ (fun ω i j ↦ X i j (ω i j)))
    (infinitePi fun i ↦ infinitePi (μ i)) = _

Premises used: Function.comp, MeasureTheory.Measure.infinitePi, MeasureTheory.Measure.map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ Measurable (β := (j : κ i) → 𝓧 i j) fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ Measurable (β := (i : ι) → (j : κ i) → 𝓧 i j) fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
    X i j (ω i j)

Tactic:
fun_prop