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)
ν : Measure ((i : ι) → X i)
hν :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
s : Finset ι
t : (i : ↥s) → Set (X (↑i : ι))
ht : ∀ (i : ↥s), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (s.restrict (π := X) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞)
  ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((↑s : Set ι).pi (α := X) fun (i : ι) ↦
        if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ) :
    ℝ≥0∞)
  (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht
-- 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)
ν : Measure ((i : ι) → X i)
hν :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
s : Finset ι
t : (i : ↥s) → Set (X (↑i : ι))
ht : ∀ (i : ↥s), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (s.restrict (π := X) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) fun (i : ι) ↦
          if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf₁ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₁ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw₂ : Eq (α := ℝ≥0∞)
  (∏ i ∈ s,
    (μ i : (a : Set (X i)) → ℝ≥0∞) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ))
  (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
Tactic: classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht
-- 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)
ν : Measure ((i : ι) → X i)
hν :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
s : Finset ι
t : (i : ↥s) → Set (X (↑i : ι))
ht : ∀ (i : ↥s), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (s.restrict (π := X) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) fun (i : ι) ↦
          if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf₁ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₁ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₂ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ s,
      (μ i : (a : Set (X i)) → ℝ≥0∞) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ))
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have a : ∀ (i : ι),
  MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
Tactic: classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht
-- 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)
ν : Measure ((i : ι) → X i)
hν :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
s : Finset ι
t : (i : ↥s) → Set (X (↑i : ι))
ht : ∀ (i : ↥s), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (s.restrict (π := X) ⁻¹' Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((ν : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) fun (i : ι) ↦
          if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hf₁ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₁ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
rw₂ :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ s,
      (μ i : (a : Set (X i)) → ℝ≥0∞) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ))
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
a :
  ∀ (i : ι),
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
hf₂ : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
hs₂ : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞)
  (∏ x ∈ s.attach,
    ((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞)
      (if h : (↑x : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑x : ι) h) else Set.univ))
  (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
Tactic: classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht
-- 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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
have h : ∀ (x : (i : ι) → X i),
  x ∈ (↑s : Set ι).pi (α := X) t ↔
    Membership.mem (γ := Set ((i : ι) → X i))
      (cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Finset ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have this : (↑s : Set ι).pi (α := X) t =
  cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
Tactic: have : Set.pi s t = cylinder s ((@Set.univ s).pi (fun i : s ↦ t i)) := by
    ext x
    simp
-- 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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
  (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
Tactic: rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
rw :
  Eq (α := ℝ≥0∞) (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
Tactic: rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
rw :
  Eq (α := ℝ≥0∞) (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hs : MeasurableSet (α := (i : ↥s) → X (↑i : ι)) (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
Tactic: rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
⊢ Eq (α := ℝ≥0∞) (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
have rw : Eq (α := ℝ≥0∞) (∏ i ∈ s.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
  (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
Tactic: rw [univ_eq_attach, prod_attach _ (fun i ↦ (μ i) (t i))]
-- 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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
this :
  (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))
rw :
  Eq (α := ℝ≥0∞) (∏ i ∈ s.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
⊢ Eq (α := ℝ≥0∞) (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
have rw₁ : Eq (α := ℝ≥0∞) (∏ x ∈ s, (μ x : (a : Set (X x)) → ℝ≥0∞) (t x)) (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i))
Tactic: rw [univ_eq_attach, prod_attach _ (fun i ↦ (μ i) (t i))]
-- 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)
I : Set ι
⊢ Eq (α := Measure ((a : (↑I : Type u_1)) → X (↑a : ι))) (map (I.restrict (π := X)) (infinitePi (X := X) μ))
    (infinitePi (X := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑I : Type u_1)) ↦ μ (↑i : ι))
have hν : ∀ (s : Finset (↑I : Type u_1)) (t : (i : (↑I : Type u_1)) → Set (X (↑i : ι))),
  (∀ (i : (↑I : Type u_1)), MeasurableSet (t i)) →
    Eq (α := ℝ≥0∞)
      ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : (↑I : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
          ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
        ℝ≥0∞)
      (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: apply eq_infinitePi
-- 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)
I : Set ι
s : Finset (↑I : Type u_1)
t : (i : (↑I : Type u_1)) → Set (X (↑i : ι))
ht : ∀ (i : (↑I : Type u_1)), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : (↑I : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hν : Eq (α := ℝ≥0∞)
  ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
      (I.restrict (π := X) ⁻¹' (↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
    ℝ≥0∞)
  (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: classical
  rw [map_apply (by fun_prop), restrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)
-- 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)
I : Set ι
s : Finset (↑I : Type u_1)
t : (i : (↑I : Type u_1)) → Set (X (↑i : ι))
ht : ∀ (i : (↑I : Type u_1)), MeasurableSet (t i)
hν :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        (I.restrict (π := X) ⁻¹' (↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : (↑I : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hν₁ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
Tactic: classical
  rw [map_apply (by fun_prop), restrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)
-- 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)
I : Set ι
s : Finset (↑I : Type u_1)
t : (i : (↑I : Type u_1)) → Set (X (↑i : ι))
ht : ∀ (i : (↑I : Type u_1)), MeasurableSet (t i)
hν :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        (I.restrict (π := X) ⁻¹' (↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hν₁ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : (↑I : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hν₂ : Eq (α := ℝ≥0∞)
  ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
      ((↑(image (Subtype.val (p := fun (x : ι) ↦ x ∈ I)) s) : Set ι).pi (α := X) fun (i : ι) ↦
        if h : i ∈ I then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) else Set.univ) :
    ℝ≥0∞)
  (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: classical
  rw [map_apply (by fun_prop), restrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)
-- 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)
I : Set ι
s : Finset (↑I : Type u_1)
t : (i : (↑I : Type u_1)) → Set (X (↑i : ι))
ht : ∀ (i : (↑I : Type u_1)), MeasurableSet (t i)
hν :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        (I.restrict (π := X) ⁻¹' (↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hν₁ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
hν₂ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        ((↑(image (Subtype.val (p := fun (x : ι) ↦ x ∈ I)) s) : Set ι).pi (α := X) fun (i : ι) ↦
          if h : i ∈ I then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) else Set.univ) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
hν₃ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : (↑I : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have hν₄ : Eq (α := ℝ≥0∞)
  (∏ i ∈ image (Subtype.val (p := fun (x : ι) ↦ x ∈ I)) s,
    (μ i : (a : Set (X i)) → ℝ≥0∞) (if h : i ∈ I then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) else Set.univ))
  (∏ i ∈ s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
Tactic: classical
  rw [map_apply (by fun_prop), restrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)
-- 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 : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
have inr : ∀
  (this :
    ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → Measure (X i))
      [hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)] {s : Set ι} (hs : Countable.{u_1 + 1} (↑s : Type u_1))
      {t : (i : ι) → Set (X i)} (mt : ∀ i ∈ s, MeasurableSet (t i)) (s_ne : Nonempty.{u_1 + 1} (↑s : Type u_1)),
      Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
        (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
          ℝ≥0∞))
  (s_ne : ¬Nonempty.{u_1 + 1} (↑s : Type u_1)),
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.pi (α := X) t) : ℝ≥0∞)
    (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) :
      ℝ≥0∞)
Tactic: wlog s_ne : Nonempty s