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_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
x : Ω
x_1 : ↥s
⊢ (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1 = s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X x_1 x

Tactic:
simp
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
⊢ Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω

Tactic:
have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
rw :
  Eq (α := Measure ((i : ↥s) → 𝓧 (↑i : ι)))
    (Measure.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) fun (i : ↥s) ↦ map (X (↑i : ι)) P)
    (Measure.pi (α := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) fun (i : ↥s) ↦ map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P)
hg :
  AEMeasurable (α := (i : ι) → 𝓧 i) (_m := MeasurableSpace.pi (X := 𝓧)) (s.restrict (π := 𝓧))
    (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
hf : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
⊢ Eq (α := Measure ((i : ↥s) → 𝓧 (↑i : ι)))
    (map (fun (ω : Ω) (i : ↥s) ↦ s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω) P)
    (Measure.pi (α := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) fun (i : ↥s) ↦ map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P)

Tactic:
rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]

Premises used: AEMeasurable.map_map_of_aemeasurable, MeasureTheory.Measure.infinitePi_map_restrict
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ Eq (α := Measure ((i : ↥s) → 𝓧 (↑i : ι)))
    (Measure.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) fun (i : ↥s) ↦ map (X (↑i : ι)) P)
    (Measure.pi (α := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) fun (i : ↥s) ↦ map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P)

Tactic:
simp
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ AEMeasurable (α := (i : ι) → 𝓧 i) (_m := MeasurableSpace.pi (X := 𝓧)) (s.restrict (π := 𝓧))
    (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P

Tactic:
mX
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P

Tactic:
exact mX
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P

Tactic:
fun i ↦ mX.eval i

Premises used: Finset.restrict, AEMeasurable.eval, Subtype.val
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
⊢ ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P

Tactic:
exact fun i ↦ mX.eval i

Premises used: AEMeasurable.eval
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : Countable ι
mX : ∀ (i : ι), AEMeasurable (X i) P
h : iIndepFun (β := 𝓧) X P
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
h.map_fun_eq_infinitePi_map₀ <| aemeasurable_pi_iff.2 mX

Premises used: Iff.mpr, aemeasurable_pi_iff, ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map₀
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
inst_1 : Countable ι
mX : ∀ (i : ι), AEMeasurable (X i) P
⊢ iIndepFun (β := 𝓧) X P ↔
    Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
      (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| aemeasurable_pi_iff.2 mX

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, aemeasurable_pi_iff
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
h : iIndepFun (β := 𝓧) X P
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
h.map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable

Premises used: Iff.mpr, measurable_pi_iff, Measurable.aemeasurable, ProbabilityTheory.iIndepFun.map_fun_eq_infinitePi_map₀
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
mX : ∀ (i : ι), Measurable (X i)
⊢ iIndepFun (β := 𝓧) X P ↔
    Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
      (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map₀ <| measurable_pi_iff.2 mX |>.aemeasurable

Premises used: Iff.mpr, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, measurable_pi_iff, Measurable.aemeasurable
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h1 : iIndepFun (β := 𝓧) X P
h2 : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
⊢ IsProbabilityMeasure P

Tactic:
have := h1.isProbabilityMeasure
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h1 : iIndepFun (β := 𝓧) X P
h2 : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
this : IsProbabilityMeasure P
rw : (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P) = infinitePi (X := 𝓧) μ
⊢ map (fun (ω : Ω) (i : ι) ↦ X i ω) P = infinitePi (X := 𝓧) μ

Tactic:
rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ h2).1 h1]

Premises used: ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, Iff.mp
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
h1 : iIndepFun (β := 𝓧) X P
h2 : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
this : IsProbabilityMeasure P
⊢ (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P) = infinitePi (X := 𝓧) μ

Tactic:
simp_rw [fun i ↦ (hX i).map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (infinitePi (X := 𝓧) μ) P
rw : infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P
⊢ iIndepFun (β := 𝓧) X P

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm, h.map_eq]

Premises used: ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map₀, ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst : IsProbabilityMeasure P
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : HasLaw (fun (ω : Ω) (i : ι) ↦ X i ω) (infinitePi (X := 𝓧) μ) P
⊢ infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P

Tactic:
simp_rw [fun i ↦ (hX i).map_eq]

Premises used: ProbabilityTheory.HasLaw.map_eq
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
⊢ ∀ (i : ι), Measurable (β := 𝓧 i) fun (ω : (i : ι) → Ω i) ↦ X i (ω i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
rw :
  Eq (α := Measure ((i : ι) → 𝓧 i)) (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) (P i))
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
⊢ iIndepFun (β := 𝓧) (fun (i : ι) (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P)

Tactic:
rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), infinitePi_map_pi _ mX]

Premises used: MeasureTheory.Measure.infinitePi_map_pi, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
congrm :
  ∀ (i : ι),
    Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) (P i))
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))

Tactic:
congrm infinitePi fun i ↦ ?_

Premises used: MeasureTheory.Measure.infinitePi
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
i : ι
⊢ Measurable (β := Ω i) fun (x : (i : ι) → Ω i) ↦ x i

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
Ω : ι → Type u_4
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
X : (i : ι) → Ω i → 𝓧 i
mX : ∀ (i : ι), Measurable (X i)
i : ι
rw :
  Eq (α := Measure (𝓧 i)) (map (X i) (map (fun (x : (i : ι) → Ω i) ↦ x i) (infinitePi (X := Ω) P)))
    (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
rw₁ :
  Eq (α := Measure (𝓧 i)) (map (X i ∘ fun (x : (i : ι) → Ω i) ↦ x i) (infinitePi (X := Ω) P))
    (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
rw₂ rw₃ :
  Eq.{u_3 + 1} (α := Measure (𝓧 i)) (map (fun (x : (i : ι) → Ω i) ↦ X i (x i)) (infinitePi (X := Ω) P))
    (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
⊢ Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))

Tactic:
rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]

Premises used: MeasureTheory.Measure.infinitePi_map_eval, Function.comp_def, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ ∀ (i : α), Measurable (β := Ω (f i)) fun (ω : (i : ι) → Ω i) ↦ ω (f i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
rw :
  Eq (α := Measure ((i : α) → Ω (f i)))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦
      map (fun (ω : (i : ι) → Ω i) ↦ ω (f i)) (infinitePi (X := Ω) P))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦ P (f i))
rw₁ : iIndepFun (β := fun (i : α) ↦ Ω (f i)) (fun (i : α) (ω : (i : ι) → Ω i) ↦ ω (f i)) (infinitePi (X := Ω) P)
⊢ Eq (α := Measure ((i : α) → Ω (f i))) (map (fun (ω : (i : ι) → Ω i) (i : α) ↦ ω (f i)) (infinitePi (X := Ω) P))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦ P (f i))

Tactic:
rw [(iIndepFun_iff_map_fun_eq_infinitePi_map <| by fun_prop).mp ?_]

Premises used: Iff.mp, ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ Eq (α := Measure ((i : α) → Ω (f i)))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦
      map (fun (ω : (i : ι) → Ω i) ↦ ω (f i)) (infinitePi (X := Ω) P))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦ P (f i))

Tactic:
simp [infinitePi_map_eval]

Premises used: MeasureTheory.Measure.infinitePi_map_eval
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ ∀ (i : ι), Measurable.{u_5, u_5} (α := Ω i) (β := Ω i) ((fun (x : ι) (ω : Ω x) ↦ ω) i)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
α : Type u_4
Ω : ι → Type u_5
mΩ : (i : ι) → MeasurableSpace (Ω i)
P : (i : ι) → Measure (Ω i)
inst : ∀ (i : ι), IsProbabilityMeasure (P i)
f : α → ι
hf : Function.Injective f
⊢ iIndepFun (β := fun (i : α) ↦ Ω (f i)) (fun (i : α) (ω : (i : ι) → Ω i) ↦ ω (f i)) (infinitePi (X := Ω) P)

Tactic:
exact .precomp hf <| iIndepFun_infinitePi (X := fun x ω ↦ ω) <| by fun_prop

Premises used: ProbabilityTheory.iIndepFun_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
⊢ IsProbabilityMeasure P

Tactic:
have := h1.isProbabilityMeasure
-- 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 : IsProbabilityMeasure P
⊢ ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)

Tactic:
have : ∀ i j, IsProbabilityMeasure (P.map (X i j)) :=
    fun i j ↦ isProbabilityMeasure_map (mX i j).aemeasurable
-- 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 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
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 : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (m0 := m𝓧 i j) (map (X i j) P)
⊢ ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)

Tactic:
have : ∀ i, IsProbabilityMeasure (P.map (fun ω ↦ (X i · ω))) :=
    fun i ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by 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 :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (x : κ i) → 𝓧 i x) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (ω : Ω) (x : κ i) ↦ X i x ω) P)
h :
  ∀ (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
⊢ 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:
ext