awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ 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)
have this : IsProbabilityMeasure P
Tactic: have := h.isProbabilityMeasure
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
have x : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
Tactic: have _ i := isProbabilityMeasure_map (mX.eval i)
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
⊢ Eq (α := Measure ((i : ι) → 𝓧 i)) (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
    (infinitePi (X := 𝓧) fun (i : ι) ↦ map (X i) P)
have refine : ∀ (s : Finset ι) (t : (i : ι) → Set (𝓧 i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
  Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
Tactic: refine eq_infinitePi _ fun s t ht ↦ ?_
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : iIndepFun (β := 𝓧) X P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have rw : ∀ (h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P)
  (this : IsProbabilityMeasure P),
  (∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)) →
    ∀ (s : Finset ι) (t : (i : ι) → Set (𝓧 i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
      Eq (α := ENNReal)
        ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) :
          ENNReal)
        (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
Tactic: rw [iIndepFun_iff_finset] at h
Cleared hypotheses: h, this, h_1, s, t, ht
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
have h₁ : ∀ (x : (i : ι) → 𝓧 i),
  x ∈ (↑s : Set ι).pi (α := 𝓧) t ↔
    Membership.mem (γ := Set ((i : ι) → 𝓧 i))
      (s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have this₁ : (↑s : Set ι).pi (α := 𝓧) t =
  s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
Tactic: have : (s : Set ι).pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
⊢ Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have rw : Eq (α := ENNReal)
  ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
      (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
    ENNReal)
  (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
Tactic: rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
rw :
  Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
⊢ Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have hg : AEMeasurable (α := (i : ι) → 𝓧 i) (_m := MeasurableSpace.pi (X := 𝓧)) (s.restrict (π := 𝓧))
  (map (fun (ω : Ω) (i : ι) ↦ X i ω) P)
Tactic: rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
rw :
  Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
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 (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have hf₁ : Measurable (α := (i : ι) → 𝓧 i) (s.restrict (π := 𝓧))
Tactic: rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
rw :
  Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
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
hf₁ : Measurable (α := (i : ι) → 𝓧 i) (s.restrict (π := 𝓧))
⊢ Eq (α := ENNReal)
    ((map (fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ι) → 𝓧 i)) → ENNReal) ((↑s : Set ι).pi (α := 𝓧) t) : ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have hs : MeasurableSet (α := (i : ↥s) → 𝓧 (↑i : ι)) (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
Tactic: rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
⊢ 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
⊢ Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this_2 :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have rw : Eq (α := ENNReal)
  (∏ i : ↥s,
    ((map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P : Measure (𝓧 (↑i : ι))) : (a : Set (𝓧 (↑i : ι))) → ENNReal)
      (t (↑i : ι)))
  (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
Tactic: rw [this, (h s).map_fun_eq_pi_map, pi_pi]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this_2 :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
rw :
  Eq (α := ENNReal)
    (∏ i : ↥s,
      ((map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P : Measure (𝓧 (↑i : ι))) : (a : Set (𝓧 (↑i : ι))) → ENNReal)
        (t (↑i : ι)))
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
⊢ Eq (α := ENNReal)
    ((map (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) P : (a : Set ((i : ↥s) → 𝓧 (↑i : ι))) → ENNReal)
        (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)) :
      ENNReal)
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i) : ENNReal)
have rw₁ : ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P
Tactic: rw [this, (h s).map_fun_eq_pi_map, pi_pi]
-- 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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this_2 :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ Eq (α := ENNReal)
    (∏ i : ↥s,
      ((map (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P : Measure (𝓧 (↑i : ι))) : (a : Set (𝓧 (↑i : ι))) → ENNReal)
        (t (↑i : ι)))
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
have simp : Eq (α := ENNReal)
  (∏ x : ↥s, ((map (X (↑x : ι)) P : Measure (𝓧 (↑x : ι))) : (a : Set (𝓧 (↑x : ι))) → ENNReal) (t (↑x : ι)))
  (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
Tactic: simp only [Finset.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
mX : AEMeasurable (β := (i : ι) → 𝓧 i) (fun (ω : Ω) (i : ι) ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
this_1 : IsProbabilityMeasure P
h_1 : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this_2 :
  (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)
this :
  Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω
⊢ Eq (α := ENNReal)
    (∏ x : ↥s, ((map (X (↑x : ι)) P : Measure (𝓧 (↑x : ι))) : (a : Set (𝓧 (↑x : ι))) → ENNReal) (t (↑x : ι)))
    (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
have rw : Eq (α := ENNReal) (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
  (∏ i ∈ s, ((map (X i) P : Measure (𝓧 i)) : (a : Set (𝓧 i)) → ENNReal) (t i))
Tactic: rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]
-- 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)
⊢ iIndepFun (β := 𝓧) X P
have x : ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)
Tactic: have _ i := isProbabilityMeasure_map (mX.eval i)
-- 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)
⊢ iIndepFun (β := 𝓧) X P
have rw : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
Tactic: rw [iIndepFun_iff_finset]
-- 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 ι
⊢ iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
have rw : 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 [iIndepFun_iff_map_fun_eq_pi_map]
-- 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 ι
rw :
  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)
⊢ iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
have rw₁ : ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P
Tactic: rw [iIndepFun_iff_map_fun_eq_pi_map]