awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
have mt : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → MeasurableSet (s i)
Tactic: rw [← coe_univ, infinitePi_pi]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
S : Set ((i : ↥s) → X (↑i : ι))
mS : MeasurableSet S
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
  ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [cylinder, ← Measure.map_apply (measurable_restrict _) mS, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
S : Set ((i : ↥s) → X (↑i : ι))
mS : MeasurableSet S
rw :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) ((map (s.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞) S : ℝ≥0∞)
  ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [cylinder, ← Measure.map_apply (measurable_restrict _) mS, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
S : Set ((i : ↥s) → X (↑i : ι))
mS : MeasurableSet S
rw :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞) S : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
  ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
      S :
    ℝ≥0∞)
Tactic: rw [cylinder, ← Measure.map_apply (measurable_restrict _) mS, infinitePi_map_restrict]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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)
⊢ Eq (α := Measure ((p : (i : ι) × κ i) → X (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))
    (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)))
have hν : ∀ (s : Finset ((i : ι) × κ i))
  (t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))),
  (∀ (i : (i : ι) × κ i), MeasurableSet (t i)) →
    Eq (α := ℝ≥0∞)
      ((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) :
            (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
          ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
            X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
        ℝ≥0∞)
      (∏ i ∈ s,
          (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞)
            (t i) :
        ℝ≥0∞)
Tactic: apply eq_infinitePi
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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)
⊢ Eq (α := ℝ≥0∞)
    ((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) :
          (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
have hν : Eq (α := ℝ≥0∞)
  (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) sorry) : 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)))
  (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) sorry,
      (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
          (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
        (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
Tactic: rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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ν :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(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)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
⊢ Eq (α := ℝ≥0∞)
    ((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) :
          (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
have hν₁ : ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
  MeasurableSet (α := (i_1 : κ i) → X i i_1)
    ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) sorry) : 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: rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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 ∈ 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))
have 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) sorry) : Set (κ i)).pi (α := fun (j : κ i) ↦ X i j) 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]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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)
⊢ Eq (α := ℝ≥0∞)
    ((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) :
          (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)
have hν : Eq (α := ℝ≥0∞)
  ((infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j :
        (a : Set ((i : ι) → (j : κ i) → X i j)) → ℝ≥0∞)
      (Set.preimage (β := (i : (i : ι) × κ i) → X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
        (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
          (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) fun (x : (i : ι) × κ i) ↦ t x)) :
    ℝ≥0∞)
  (∏ i ∈ s,
      (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
    ℝ≥0∞)
Tactic: classical
  rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]
  · exact Finset.prod_congr rfl (fun _ _ ↦ infinitePi_pi _ fun _ _ ↦ ht _)
  · simp only [mem_image, Sigma.exists, exists_and_right, exists_eq_right, forall_exists_index]
    exact fun i j hij ↦ MeasurableSet.pi (countable_toSet _) fun k hk ↦ by simp_all
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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)
⊢ 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)
have 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))
Tactic: rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_piCurry_symm]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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))
⊢ 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)
have 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)))
Tactic: rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_piCurry_symm]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ 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)
have 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))
Tactic: rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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))
⊢ 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)
have hg : Measurable (α := (b : ι × κ) → X) (β := (a : (_ : ι) × κ) → X)
  (⇑(piCongrLeft (fun (x : (_ : ι) × κ) ↦ X) (Equiv.sigmaEquivProd ι κ).symm :
        ((b : ι × κ) → X) ≃ᵐ ((a : (_ : ι) × κ) → X)) :
    (a : (b : ι × κ) → X) → (a : (_ : ι) × κ) → X)
Tactic: rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
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)
⊢ 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)
have hf : Measurable (α := ι → κ → X) (β := (b : ι × κ) → X)
  (⇑(MeasurableEquiv.symm (MeasurableEquiv.curry ι κ X)) : (a : ι → κ → X) → ι × κ → X)
Tactic: rw [← (MeasurableEquiv.piCongrLeft (fun _ ↦ X)
    (Equiv.sigmaEquivProd ι κ).symm).map_measurableEquiv_injective.eq_iff, map_map]