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)
I : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞) s : ℝ≥0∞)
    (((fun (I : Finset ι) ↦
              (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
            I :
          (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : MeasurableSpace.pi (X := X) = MeasurableSpace.generateFrom (measurableCylinders X)
Tactic: rw [map_apply (measurable_restrict I) hs, infinitePi, dif_pos hμ, AddContent.measure_eq,
    ← cylinder, piContent_cylinder μ hs]
-- 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 : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
h : MeasurableSpace.pi (X := X) = MeasurableSpace.generateFrom (measurableCylinders X)
⊢ Eq (α := ℝ≥0∞)
    ((map (I.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞) s : ℝ≥0∞)
    (((fun (I : Finset ι) ↦
              (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
            I :
          (a : Set ((i : ↥I) → X (↑i : ι))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : I.restrict (π := X) ⁻¹' s ∈ measurableCylinders X
Tactic: rw [map_apply (measurable_restrict I) hs, infinitePi, dif_pos hμ, AddContent.measure_eq,
    ← cylinder, piContent_cylinder μ hs]
-- 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)
⊢ IsProbabilityMeasure (infinitePi (X := X) μ)
have measure_univ : Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
Tactic: constructor
-- 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)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ : Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) ∅ Set.univ) : ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]
-- 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_univ :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) ∅ Set.univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₁ : Eq (α := ℝ≥0∞)
  ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      (Set.preimage (β := (i : ↥∅) → X (↑i : ι)) (Finset.restrict (π := X) ∅) Set.univ) :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]
-- 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_univ :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) ∅ Set.univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₁ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ↥∅) → X (↑i : ι)) (Finset.restrict (π := X) ∅) Set.univ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₂ : Eq (α := ℝ≥0∞)
  ((map (Finset.restrict (π := X) ∅) (infinitePi (X := X) μ) : (a : Set ((i : ↥∅) → X (↑i : ι))) → ℝ≥0∞) Set.univ :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]
-- 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_univ :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) ∅ Set.univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₁ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ↥∅) → X (↑i : ι)) (Finset.restrict (π := X) ∅) Set.univ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₂ :
  Eq (α := ℝ≥0∞)
    ((map (Finset.restrict (π := X) ∅) (infinitePi (X := X) μ) : (a : Set ((i : ↥∅) → X (↑i : ι))) → ℝ≥0∞) Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₃ : Eq (α := ℝ≥0∞)
  ((Measure.pi (α := fun (i : ↥∅) ↦ X (↑i : ι)) fun (i : ↥∅) ↦ μ (↑i : ι) : (a : Set ((i : ↥∅) → X (↑i : ι))) → ℝ≥0∞)
      Set.univ :
    ℝ≥0∞)
  (1 : ℝ≥0∞)
Tactic: rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]
-- 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_univ :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) ∅ Set.univ) : ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₁ :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ↥∅) → X (↑i : ι)) (Finset.restrict (π := X) ∅) Set.univ) :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₂ :
  Eq (α := ℝ≥0∞)
    ((map (Finset.restrict (π := X) ∅) (infinitePi (X := X) μ) : (a : Set ((i : ↥∅) → X (↑i : ι))) → ℝ≥0∞) Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
measure_univ₃ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥∅) ↦ X (↑i : ι)) fun (i : ↥∅) ↦ μ (↑i : ι) : (a : Set ((i : ↥∅) → X (↑i : ι))) → ℝ≥0∞)
        Set.univ :
      ℝ≥0∞)
    (1 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have measure_univ₄ : Eq (α := ℝ≥0∞) 1 1
Tactic: rw [← cylinder_univ ∅, cylinder, ← map_apply (measurable_restrict _) .univ,
    infinitePi_map_restrict, measure_univ]
-- 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∞)
⊢ ν = infinitePi (X := X) μ
have refine : IsProjectiveLimit (α := X) ν fun (I : Finset ι) ↦ Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)
Tactic: refine (isProjectiveLimit_infinitePi μ).unique ?_ |>.symm
-- 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∞)
⊢ IsProjectiveLimit (α := X) ν fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)
have refine : ∀ (s : Finset ι) (t : (i : ↥s) → Set (X (↑i : ι))) (ht : ∀ (i : ↥s), MeasurableSet (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∞)
Tactic: refine fun s ↦ (pi_eq fun t ht ↦ ?_).symm
-- 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)
⊢ 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.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
Tactic: rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
-- 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∞)
    (∏ 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.attach, ((μ (↑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: rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
-- 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∞)
    (∏ 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.attach, ((μ (↑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)
⊢ 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 hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
Tactic: rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
-- 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∞)
    (∏ 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.attach, ((μ (↑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))
⊢ 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 hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
Tactic: rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
-- 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)
⊢ 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.attach, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i))
have e_f : ∀ (i : ↥s),
  Eq (α := ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
        (if h : (↑i : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) h) else Set.univ) :
      ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: congr with 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)
ν : 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)
i : ↥s
⊢ Eq (α := ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
        (if h : (↑i : ι) ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) h) else Set.univ) :
      ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
have e_f : Eq (α := ℝ≥0∞)
  (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
      (t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) sorry)) :
    ℝ≥0∞)
  (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
Tactic: rw [dif_pos i.2]
-- 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)
i : ι
⊢ MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
have pos : ∀ (hi : i ∈ s),
  MeasurableSet (α := X i)
    (t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)))
Tactic: split_ifs with hi
-- 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)
i : ι
pos :
  ∀ (hi : i ∈ s),
    MeasurableSet (α := X i)
      (t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i hi) : ι)))
⊢ MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)
have neg : ∀ (hi : i ∉ s), MeasurableSet.{u_2} (α := X i) Set.univ
Tactic: split_ifs with hi
-- 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)
⊢ 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.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∞)
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∞)
⊢ 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 hf : Measurable (α := (i : ι) → X i) (s.restrict (π := X))
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))
⊢ 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 hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
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