awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
hν :
  ∀ (i : ι) (x : κ i) (h : Sigma.mk (β := fun (a : ι) ↦ κ a) i x ∈ s),
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦ X i j)
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
⊢ ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))

Tactic:
simp only [mem_image, Sigma.exists, exists_and_right, exists_eq_right, forall_exists_index]

Premises used: Finset.mem_image, Sigma.exists, forall_exists_index, exists_eq_right, exists_and_right
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
i : ι
j : κ i
hij : Sigma.mk (β := fun (a : ι) ↦ κ a) i j ∈ s
k : κ i
hk : k ∈ (↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i))
⊢ MeasurableSet (α := X i k)
    (t (Sigma.mk (β := fun (i : ι) ↦ κ i) i k) :
      Set
        (X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i k).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i k).snd (β := fun (i : ι) ↦ κ i))))

Tactic:
simp_all
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ ∀ (i : ι) (x : κ i) (h : Sigma.mk (β := fun (a : ι) ↦ κ a) i x ∈ s),
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦ X i j)
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))

Tactic:
exact fun i j hij ↦ MeasurableSet.pi (countable_toSet _) fun k hk ↦ by simp_all

Premises used: Finset.countable_toSet, MeasurableSet.pi
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
rw :
  Eq (α := Measure ((p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      fun (p : (i : ι) × κ i) ↦ μ (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (map (α := (i : ι) → (j : κ i) → X i j)
      (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
        (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j))
rw₁ rw₂ :
  Eq (α := Measure ((p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      fun (p : (i : ι) × κ i) ↦ μ (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
    (infinitePi (X := fun (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      fun (p : (i : ι) × κ i) ↦ μ (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
⊢ Eq (α := Measure ((i : ι) → (j : κ i) → X i j))
    (map (α := (p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      (⇑(piCurry (κ := κ) X) : (a : (p : (i : ι) × κ i) → X p.fst p.snd) → (i : ι) → (j : κ i) → X i j)
      (infinitePi (X := fun (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
        fun (p : (i : ι) × κ i) ↦ μ (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j)

Tactic:
rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_piCurry_symm]

Premises used: MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, MeasureTheory.Measure.infinitePi_map_piCurry_symm
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
rw :
  Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (map (α := ι → κ → X)
      (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
hg :
  Measurable (α := (b : ι × κ) → X) (β := (a : (_ : ι) × κ) → X)
    (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
          ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
      (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
hf :
  Measurable (α := ι → κ → X) (β := (b : ι × κ) → X)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
⊢ Eq (α := Measure (ι × κ → X))
    (map (α := ι → κ → X) (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
    (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)

Tactic:
rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]

Premises used: Function.Injective.eq_iff, MeasurableEquiv.piCongrLeft, MeasurableEquiv.map_measurableEquiv_injective, Equiv.symm, MeasureTheory.Measure.map_map, Equiv.sigmaEquivProd
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
h :
  ∀ (x : ι → κ → X) (x_1 : (_ : ι) × κ),
    Eq.{u_8 + 1} (α := X)
      (Function.comp (β := (b : ι × κ) → X)
          (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
                ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
            (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
          (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X) x x_1 :
        X)
      ((MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_2 : κ) ↦ X) :
            (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
          x x_1 :
        X)
⊢ Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)

Tactic:
ext
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
x : ι → κ → X
x_1 : (_ : ι) × κ
⊢ Eq.{u_8 + 1} (α := X)
    (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X) x x_1 :
      X)
    ((MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_2 : κ) ↦ X) :
          (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
        x x_1 :
      X)

Tactic:
simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]

Premises used: Sigma.uncurry, MeasurableEquiv.piCongrLeft, Equiv.piCongrLeft
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)

Tactic:
have : (MeasurableEquiv.piCongrLeft (fun _ ↦ X) (Equiv.sigmaEquivProd ι κ).symm) ∘
        (MeasurableEquiv.curry ι κ X).symm = ⇑(MeasurableEquiv.piCurry (fun _ _ ↦ X)).symm := by
      ext; simp [piCongrLeft, Equiv.piCongrLeft, Sigma.uncurry]
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
rw :
  Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (infinitePi (X := fun (p : (_ : ι) × κ) ↦ X) fun (p : (_ : ι) × κ) ↦
      μ (p.fst (β := fun (i : ι) ↦ κ)) (p.snd (β := fun (i : ι) ↦ κ)))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
⊢ Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (map (α := ι → κ → X)
      (Function.comp (β := (b : ι × κ) → X)
        (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
              ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
          (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
        (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))

Tactic:
rw [this, infinitePi_map_piCurry_symm]

Premises used: MeasureTheory.Measure.infinitePi_map_piCurry_symm
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
⊢ Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (infinitePi (X := fun (p : (_ : ι) × κ) ↦ X) fun (p : (_ : ι) × κ) ↦
      μ (p.fst (β := fun (x : ι) ↦ κ)) (p.snd (β := fun (x : ι) ↦ κ)))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (p : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (i : ι × κ) ↦ X) fun (i : ι × κ) ↦
        μ (Sigma.fst (β := fun (x : ι) ↦ κ) (((Equiv.sigmaEquivProd ι κ).symm : (a : ι × κ) → (_ : ι) × κ) i))
          (Sigma.snd (β := fun (x : ι) ↦ κ) (((Equiv.sigmaEquivProd ι κ).symm : (a : ι × κ) → (_ : ι) × κ) i))))

Tactic:
infinitePi_map_piCongrLeft (fun p ↦ μ p.1 p.2) (Equiv.sigmaEquivProd ι κ).symm |>.symm

Premises used: MeasureTheory.Measure.infinitePi_map_piCongrLeft, Equiv.symm, Eq.symm, Equiv.sigmaEquivProd
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
this :
  Eq (α := (ι → κ → X) → (a : (_ : ι) × κ) → X)
    (Function.comp (β := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X))
    (⇑(MeasurableEquiv.symm (piCurry.{u_6, u_7, u_8} (κ := fun (i : ι) ↦ κ) fun (x : ι) (x_1 : κ) ↦ X)) :
      (a : (i : ι) → (j : κ) → X) → (p : (_ : ι) × κ) → X)
⊢ Eq (α := Measure ((a : (_ : ι) × κ) → X))
    (infinitePi (X := fun (p : (_ : ι) × κ) ↦ X) fun (p : (_ : ι) × κ) ↦
      μ (p.fst (β := fun (i : ι) ↦ κ)) (p.snd (β := fun (i : ι) ↦ κ)))
    (map (α := (b : ι × κ) → X)
      (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
            ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
        (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))

Tactic:
convert! infinitePi_map_piCongrLeft (fun p ↦ μ p.1 p.2) (Equiv.sigmaEquivProd ι κ).symm |>.symm

Premises used: MeasureTheory.Measure.infinitePi_map_piCongrLeft, Equiv.symm, Eq.symm, Equiv.sigmaEquivProd
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable (α := (b : ι × κ) → X) (β := (a : (_ : ι) × κ) → X)
    (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
          ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
      (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ Measurable (α := ι → κ → X) (β := (b : ι × κ) → X)
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
rw :
  Eq (α := Measure (ι × κ → X)) (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
    (map (α := ι → κ → X) (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
      (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j))
rw₁ rw₂ :
  Eq (α := Measure (ι × κ → X)) (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
    (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2)
⊢ Eq (α := Measure (ι → κ → X))
    (map (α := ι × κ → X) (⇑(MeasurableEquiv.curry ι κ X) : (a : ι × κ → X) → ι → κ → X)
      (infinitePi (X := fun (p : ι × κ) ↦ X) fun (p : ι × κ) ↦ μ p.1 p.2))
    (infinitePi (X := fun (i : ι) ↦ (i : κ) → X) fun (i : ι) ↦ infinitePi (X := fun (j : κ) ↦ X) fun (j : κ) ↦ μ i j)

Tactic:
rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_curry_symm]

Premises used: MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, MeasureTheory.Measure.infinitePi_map_curry_symm
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → E
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
hφ : AEMeasurable (s.restrict (π := X)) (infinitePi (X := X) μ)
hfm :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ))
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦ f y)

Tactic:
rw [← integral_map, infinitePi_map_restrict]

Premises used: MeasureTheory.integral_map, MeasureTheory.Measure.infinitePi_map_restrict
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → E
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
⊢ AEMeasurable (s.restrict (π := X)) (infinitePi (X := X) μ)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → E
hf hfm hfm₁ hfm₂ hfm₃ :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
⊢ AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) f
    (Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ))

Tactic:
rwa [infinitePi_map_restrict]

Premises used: MeasureTheory.Measure.infinitePi_map_restrict
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
f : ((i : ↥s) → X (↑i : ι)) → ℝ≥0∞
hf : Measurable f
rw :
  ∫⁻ (a : (i : ↥s) → X (↑i : ι)), f a ∂Measure.map (s.restrict (π := X)) (infinitePi (X := X) μ) =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
rw₁ rw₂ :
  ∫⁻ (a : (i : ↥s) → X (↑i : ι)),
      f
        a ∂(fun (I : Finset ι) ↦
          (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
        s =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)
⊢ ∫⁻ (y : (i : ι) → X i), f (s.restrict (π := X) y) ∂infinitePi (X := X) μ =
    ∫⁻ (y : (i : ↥s) → X (↑i : ι)), f y ∂Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)

Tactic:
rw [← lintegral_map hf (measurable_restrict _), isProjectiveLimit_infinitePi μ]

Premises used: Finset.measurable_restrict, MeasureTheory.Measure.isProjectiveLimit_infinitePi, MeasureTheory.lintegral_map
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
y : (i : ι) → X i
i : ι
hi : i ∈ (↑s : Set ι)
⊢ Function.updateFinset (π := X) x s (s.restrict (π := X) y) i = y i

Tactic:
simp_all [Function.updateFinset]

Premises used: Function.updateFinset
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
⊢ ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y

Tactic:
have this y : g (s.restrict y) = f y :=
    mf.dependsOn_of_piFinset fun i hi ↦ by simp_all [Function.updateFinset]
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : DecidableEq ι
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
s : Finset ι
f : ((i : ι) → X i) → E
mf : StronglyMeasurable f
x : (i : ι) → X i
g : ((i : ↥s) → X (↑i : ι)) → E := fun (y : (i : ↥s) → X (↑i : ι)) ↦ f (Function.updateFinset (π := X) x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict (π := X) y) = f y
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι))) g
    (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι))
⊢ Eq.{u_3 + 1} (α := E) (∫ (y : (i : ι) → X i), f y ∂infinitePi (X := X) μ)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥s) ↦ X (↑i : ι)))
      (Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι)) fun (y : (i : ↥s) → X (↑i : ι)) ↦
      f (Function.updateFinset (π := X) x s y))

Tactic:
rw [← integral_congr_ae <| ae_of_all _ this, integral_restrict_infinitePi]

Premises used: MeasureTheory.integral_congr_ae, MeasureTheory.ae_of_all, MeasureTheory.integral_restrict_infinitePi