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
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)
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)
⊢ 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

Premises used: ProbabilityTheory.iIndepFun_iff_finset
-- 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 : 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)
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
⊢ (↑s : Set ι).pi (α := 𝓧) t =
    s.restrict (π := 𝓧) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι)

Tactic:
ext
-- 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 : 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)
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:
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
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 : ι)

Tactic:
have : (s : Set ι).pi t = s.restrict ⁻¹' (Set.univ.pi fun i ↦ t 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
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 (π := 𝓧))
hs :
  MeasurableSet (α := (i : ↥s) → 𝓧 (↑i : ι))
    (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)

Tactic:
rw [this, ← map_apply, AEMeasurable.map_map_of_aemeasurable]

Premises used: MeasureTheory.Measure.map_apply, AEMeasurable.map_map_of_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
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 : ι)
h₁ :
  ∀ (x : Ω) (x_1 : ↥s),
    (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1 = s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X x_1 x
⊢ Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω

Tactic:
ext
-- 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 : 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 : ι)
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
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 ω

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
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))
rw₁ : ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P
⊢ 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, (h s).map_fun_eq_pi_map, pi_pi]

Premises used: MeasureTheory.Measure.pi_pi, ProbabilityTheory.iIndepFun.map_fun_eq_pi_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
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 ω
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))
⊢ 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:
simp only [Finset.restrict]

Premises used: Finset.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
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 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))
⊢ 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:
rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]

Premises used: Finset.prod_coe_sort, MeasureTheory.Measure.map, DFunLike.coe
-- 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 : 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 ω
⊢ ∀ (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
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 ω
⊢ ∀ (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
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 : ι)
⊢ 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
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 : ι)
⊢ Measurable (α := (i : ι) → 𝓧 i) (s.restrict (π := 𝓧))

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
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 : ι)
⊢ 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
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 : ι)
⊢ 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
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 : ι)
⊢ MeasurableSet (α := (i : ↥s) → 𝓧 (↑i : ι))
    (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))

Tactic:
.univ_pi fun i ↦ ht i

Premises used: Subtype.val, MeasurableSet.univ_pi
-- 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 : 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 : ι)
⊢ MeasurableSet (α := (i : ↥s) → 𝓧 (↑i : ι))
    (Set.pi (α := fun (i : ↥s) ↦ 𝓧 (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))

Tactic:
exact .univ_pi fun i ↦ ht i
-- 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)
⊢ ∀ (i : ι), IsProbabilityMeasure.{u_3} (α := 𝓧 i) (m0 := m𝓧 i) (map (fun (x : Ω) ↦ X i x) P)

Tactic:
have _ i := isProbabilityMeasure_map (mX.eval i)
-- 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)
rw : ∀ (s : Finset ι), iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P
⊢ iIndepFun (β := 𝓧) X P

Tactic:
rw [iIndepFun_iff_finset]

Premises used: ProbabilityTheory.iIndepFun_iff_finset
-- 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 ι
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)
rw₁ : ∀ (i : ↥s), AEMeasurable (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i) P
⊢ iIndepFun (β := fun (x : ↥s) ↦ 𝓧 (↑x : ι)) (s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X) P

Tactic:
rw [iIndepFun_iff_map_fun_eq_pi_map]

Premises used: ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_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 : 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 ι
h₁ :
  ∀ (x : Ω) (x_1 : ↥s),
    (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) x x_1 = s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X x_1 x
⊢ Eq (α := Ω → (i : ↥s) → 𝓧 (↑i : ι)) (s.restrict (π := 𝓧) ∘ fun (ω : Ω) (i : ι) ↦ X i ω) fun (ω : Ω) (i : ↥s) ↦
    s.restrict (π := fun (i : ι) ↦ Ω → 𝓧 i) X i ω

Tactic:
ext