awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 ω
have h₁ : ∀ (x : Ω) (x_1 : ↥s),
  (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1 = s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X x_1 x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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 (α := 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)
have this : 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
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 : ι)))
    (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)
have 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)
Tactic: rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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)
⊢ 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)
have hg : AEMeasurable (α := (i : ι) → 𝓧 i) (_m := MeasurableSpace.pi (X := 𝓧)) (s.restrict (π := 𝓧))
  (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
Tactic: rw [← this, ← AEMeasurable.map_map_of_aemeasurable, h, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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
⊢ map (fun (ω : Ω) (i : ι) ↦ X i ω) P = infinitePi (X := 𝓧) μ
have this : IsProbabilityMeasure P
Tactic: have := h1.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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
⊢ map (fun (ω : Ω) (i : ι) ↦ X i ω) P = infinitePi (X := 𝓧) μ
have rw : (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P) = infinitePi (X := 𝓧) μ
Tactic: rw [(iIndepFun_iff_map_fun_eq_infinitePi_map₀ h2).1 h1]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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
⊢ iIndepFun (β := 𝓧) X P
have rw : infinitePi (X := 𝓧) μ = infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P
Tactic: rw [iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm, h.map_eq]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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)
⊢ iIndepFun (β := 𝓧) (fun (i : ι) (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P)
have 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))
Tactic: rw [iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop), infinitePi_map_pi _ mX]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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)
⊢ 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))
have congrm : ∀ (i : ι), Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
Tactic: congrm infinitePi fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 : ι
⊢ Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
have 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))
Tactic: rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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))
⊢ Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
have 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))
Tactic: rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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))
⊢ Eq (α := Measure (𝓧 i)) (map (X i) (P i)) (map (fun (ω : (i : ι) → Ω i) ↦ X i (ω i)) (infinitePi (X := Ω) P))
have 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))
Tactic: rw [← infinitePi_map_eval P i, map_map (mX i) (by fun_prop), Function.comp_def]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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))) (map (fun (ω : (i : ι) → Ω i) (i : α) ↦ ω (f i)) (infinitePi (X := Ω) P))
    (infinitePi (X := fun (i : α) ↦ Ω (f i)) fun (i : α) ↦ P (f i))
have 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))
Tactic: rw [(iIndepFun_iff_map_fun_eq_infinitePi_map <| by fun_prop).mp ?_]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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))
⊢ 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))
have rw₁ : iIndepFun (β := fun (i : α) ↦ Ω (f i)) (fun (i : α) (ω : (i : ι) → Ω i) ↦ ω (f i)) (infinitePi (X := Ω) P)
Tactic: rw [(iIndepFun_iff_map_fun_eq_infinitePi_map <| by fun_prop).mp ?_]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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
⊢ 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
have this : IsProbabilityMeasure P
Tactic: have := h1.isProbabilityMeasure
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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
⊢ 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
have this₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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)
⊢ 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
have this₁ : ∀ (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))
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 ω
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (hypothesis)
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)
⊢ 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
have 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 ω
Tactic: have : (MeasurableEquiv.piCurry 𝓧) ∘ (fun ω p ↦ X p.1 p.2 ω) = fun ω i j ↦ X i j ω := by
    ext; simp [Sigma.curry]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 ω
⊢ 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
have 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)
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))]
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 ω
⊢ 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)
have 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)
Tactic: congrm infinitePi fun i ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Independence.InfinitePi (goal)
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 : ι
⊢ 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)
have 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)
Tactic: rw [(iIndepFun_iff_map_fun_eq_infinitePi_map (by fun_prop)).1 (h2 i)]