awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
refine_2 :
  Eq (α := Measure ((j : κ i) → 𝓧 i j)) (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦ map (X i i_1) (μ i i_1))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
refine_2₁ : ∀ (i_1 : κ i), Measurable (X i i_1)
rw :
  ∀ (i : ι),
    IsProbabilityMeasure (α := (j : κ i) → 𝓧 i j) (m0 := MeasurableSpace.pi (X := 𝓧 i))
      (map (fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)) (infinitePi (X := Ω i) (μ i)))
refine_2₂ :
  ∀ (i : ι), Measurable (β := (j : κ i) → 𝓧 i j) fun (f : (fun (i : ι) ↦ (j : κ i) → Ω i j) i) (j : κ i) ↦ X i j (f j)
⊢ Eq (α := Measure ((j : κ i) → 𝓧 i j))
    (map (α := (i : ι) → (i_1 : κ i) → Ω i i_1)
      ((fun (f : (i : ι) → (j : κ i) → 𝓧 i j) ↦ f i) ∘ fun (ω : (i : ι) → (i_1 : κ i) → Ω i i_1) (i : ι) (j : κ i) ↦
        X i j (ω i j))
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → Ω i i_1) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))
    (infinitePi (X := 𝓧 i) fun (i_1 : κ i) ↦
      map (α := (i : ι) → (i_2 : κ i) → Ω i i_2)
        ((fun (i : ι) (j : κ i) (ω : (i : ι) → (i_2 : κ i) → Ω i i_2) ↦ X i j (ω i j)) i i_1)
        (infinitePi (X := fun (i : ι) ↦ (i_2 : κ i) → Ω i i_2) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i)))

Tactic:
rw [← map_map (by fun_prop) (by fun_prop),
    infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j) (μ := fun i ↦ infinitePi (μ i))
      (f := fun i f j ↦ X i j (f j)), @infinitePi_map_eval .., infinitePi_map_pi]

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

Tactic:
congrm infinitePi fun j ↦ ?_

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

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

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

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

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

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

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

Tactic:
rw [← map_map (by fun_prop) (by fun_prop), infinitePi_map_pi (X := fun i ↦ (j : κ i) → Ω i j)
        (μ := fun i ↦ infinitePi (μ i)) (f := fun i f j ↦ X i j (f j)),
        ← map_map (by fun_prop) (by fun_prop),
        @infinitePi_map_eval .., infinitePi_map_pi, @infinitePi_map_eval ..]

Premises used: MeasureTheory.Measure.infinitePi, MeasureTheory.Measure.infinitePi_map_eval, MeasureTheory.Measure.infinitePi_map_pi, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
j : κ i
⊢ ∀ (i_1 : κ i), Measurable (X i i_1)

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

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

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

Tactic:
exact fun _ ↦ isProbabilityMeasure_map (by fun_prop)

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

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

Tactic:
exact fun _ ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop))

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
Ω : (i : ι) → κ i → Type u_6
mΩ : (i : ι) → (j : κ i) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ i) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ i) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
i : ι
⊢ ∀ (i_1 : κ i), Measurable (X i i_1)

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

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

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

Tactic:
exact fun _ ↦ isProbabilityMeasure_map (Measurable.aemeasurable (by fun_prop))

Premises used: Measurable.aemeasurable, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : Type u_4
𝓧 : ι → κ → Type u_5
m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ), Measurable (X i j)
h1 : iIndepFun (β := fun (i : ι) ↦ (x : κ) → 𝓧 i x) (fun (i : ι) (ω : Ω) (x : κ) ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (β := 𝓧 i) (X i) P
⊢ iIndepFun (β := fun (p : ι × κ) ↦ 𝓧 p.1 p.2) (fun (p : ι × κ) (ω : Ω) ↦ X p.1 p.2 ω) P

Tactic:
(iIndepFun_uncurry mX h1 h2).of_precomp (Equiv.sigmaEquivProd ι κ).surjective

Premises used: ProbabilityTheory.iIndepFun.of_precomp, ProbabilityTheory.iIndepFun_uncurry, Equiv.surjective, Equiv.sigmaEquivProd
-- Module: Mathlib.Probability.Independence.InfinitePi
Goal:
ι : Type u_1
κ : Type u_4
𝓧 : ι → κ → Type u_5
m𝓧 : (i : ι) → (j : κ) → MeasurableSpace (𝓧 i j)
Ω : ι → κ → Type u_6
mΩ : (i : ι) → (j : κ) → MeasurableSpace (Ω i j)
X : (i : ι) → (j : κ) → Ω i j → 𝓧 i j
μ : (i : ι) → (j : κ) → Measure (Ω i j)
inst : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
mX : ∀ (i : ι) (j : κ), Measurable (X i j)
⊢ iIndepFun (_mΩ := MeasurableSpace.pi (X := fun (i : ι) ↦ (j : κ) → Ω i j)) (β := fun (p : ι × κ) ↦ 𝓧 p.1 p.2)
    (fun (p : ι × κ) (ω : (i : ι) → (j : κ) → Ω i j) ↦ X p.1 p.2 (ω p.1 p.2))
    (infinitePi (X := fun (i : ι) ↦ (j : κ) → Ω i j) fun (i : ι) ↦ infinitePi (X := Ω i) (μ i))

Tactic:
(iIndepFun_uncurry_infinitePi μ mX).of_precomp (Equiv.sigmaEquivProd ι κ).surjective

Premises used: ProbabilityTheory.iIndepFun.of_precomp, ProbabilityTheory.iIndepFun_uncurry_infinitePi, Equiv.surjective, Equiv.sigmaEquivProd
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
f : Ω → ℝ≥0∞
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_meas_f : Measurable f
revert :
  ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
    (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
revert f
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
⊢ ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a

Tactic:
have h_mul_indicator : ∀ g, Measurable g → Measurable fun a => g a * T.indicator (fun _ => c) a :=
    fun g h_mg => h_mg.mul (measurable_const.indicator h_meas_T)
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
indicator :
  ∀ (c_1 : ℝ≥0∞) ⦃s : Set Ω⦄,
    MeasurableSet s →
      ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s.indicator (fun (x : Ω) ↦ c_1) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
        (∫⁻ (ω : Ω), s.indicator (fun (x : Ω) ↦ c_1) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
add :
  ∀ ⦃f g : Ω → ℝ≥0∞⦄,
    Disjoint (Function.support f) (Function.support g) →
      Measurable f →
        Measurable g →
          ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ →
            ∫⁻ (ω : Ω), g ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
                (∫⁻ (ω : Ω), g ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ →
              ∫⁻ (ω : Ω), (f + g) ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
                (∫⁻ (ω : Ω), (f + g) ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
iSup :
  ∀ ⦃f : ℕ → Ω → ℝ≥0∞⦄,
    (∀ (n : ℕ), Measurable (f n)) →
      Monotone f →
        (∀ (n : ℕ),
            ∫⁻ (ω : Ω), f n ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
              (∫⁻ (ω : Ω), f n ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ) →
          ∫⁻ (ω : Ω),
              HMul.hMul (α := ℝ≥0∞) ((fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
            (∫⁻ (ω : Ω), (fun (x : Ω) ↦ (⨆ (n : ℕ), f n x : ℝ≥0∞)) ω ∂μ) *
              ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∀ {f : Ω → ℝ≥0∞} (h_meas_f : Measurable f),
    ∫⁻ (ω : Ω), f ω * T.indicator (fun (x : Ω) ↦ c) ω ∂μ =
      (∫⁻ (ω : Ω), f ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
apply @Measurable.ennreal_induction _ Mf

Premises used: Measurable.ennreal_induction
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
indicator :
  ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun (j : Ω) ↦ c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun (x : Ω) ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ
⊢ ∫⁻ (ω : Ω), HMul.hMul (α := ℝ≥0∞) (s'.indicator (fun (x : Ω) ↦ c') ω) (T.indicator (fun (x : Ω) ↦ c) ω) ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun (x : Ω) ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
simp_rw [← inter_indicator_mul]

Premises used: Set.inter_indicator_mul
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
indicator : ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ
⊢ ∫⁻ (ω : Ω), (s' ∩ T).indicator (fun (j : Ω) ↦ c' * c) ω ∂μ =
    (∫⁻ (ω : Ω), s'.indicator (fun (x : Ω) ↦ c') ω ∂μ) * ∫⁻ (ω : Ω), T.indicator (fun (x : Ω) ↦ c) ω ∂μ

Tactic:
rw [lintegral_indicator (MeasurableSet.inter (hMf _ h_meas_s') h_meas_T),
      lintegral_indicator (hMf _ h_meas_s'), lintegral_indicator h_meas_T]

Premises used: MeasureTheory.lintegral_indicator, MeasurableSet.inter
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
indicator :
  HMul.hMul (β := ℝ≥0∞) (c' * c) ((μ : (a : Set Ω) → ℝ≥0∞) (s' ∩ T) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)
⊢ ∫⁻ (a : Ω) in s' ∩ T, c' * c ∂μ = (∫⁻ (a : Ω) in s', c' ∂μ) * ∫⁻ (a : Ω) in T, c ∂μ

Tactic:
simp only [lintegral_const, univ_inter,
      MeasurableSet.univ, Measure.restrict_apply]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_apply, Set.univ_inter, MeasurableSet.univ
-- Module: Mathlib.Probability.Independence.Integration
Goal:
Ω : Type u_1
Mf mΩ : MeasurableSpace Ω
μ : Measure Ω
hMf : Mf ≤ mΩ
c : ℝ≥0∞
T : Set Ω
h_meas_T : MeasurableSet T
h_ind : IndepSets {s : Set Ω | MeasurableSet s} {T} μ
h_mul_indicator :
  ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a
c' : ℝ≥0∞
s' : Set Ω
h_meas_s' : MeasurableSet s'
indicator :
  ∀
    (h_ind :
      ∀ (t1 t2 : Set Ω),
        Membership.mem (γ := Set (Set Ω)) {s : Set Ω | MeasurableSet s} t1 →
          Membership.mem (γ := Set (Set Ω)) {T} t2 →
            (μ : (a : Set Ω) → ℝ≥0∞) (t1 ∩ t2) =
              HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set Ω) → ℝ≥0∞) t1 : ℝ≥0∞)
                ((μ : (a : Set Ω) → ℝ≥0∞) t2 : ℝ≥0∞))
    (h_mul_indicator :
      ∀ (g : Ω → ℝ≥0∞), Measurable g → Measurable (β := ℝ≥0∞) fun (a : Ω) ↦ g a * T.indicator (fun (x : Ω) ↦ c) a)
    (c' : ℝ≥0∞) ⦃s' : Set Ω⦄ (h_meas_s' : MeasurableSet s'),
    HMul.hMul (β := ℝ≥0∞) (c' * c) ((μ : (a : Set Ω) → ℝ≥0∞) (s' ∩ T) : ℝ≥0∞) =
      HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) *
        HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)
⊢ HMul.hMul (β := ℝ≥0∞) (c' * c) ((μ : (a : Set Ω) → ℝ≥0∞) (s' ∩ T) : ℝ≥0∞) =
    HMul.hMul (β := ℝ≥0∞) c' ((μ : (a : Set Ω) → ℝ≥0∞) s' : ℝ≥0∞) *
      HMul.hMul (β := ℝ≥0∞) c ((μ : (a : Set Ω) → ℝ≥0∞) T : ℝ≥0∞)

Tactic:
rw [IndepSets_iff] at h_ind

Premises used: ProbabilityTheory.IndepSets_iff