awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
ν : 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)
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∞)
⊢ 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:
congr with i
-- 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)
ν : 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
e_f e_f₁ :
  Eq (α := ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞)
        (t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) (↑i : ι) ⋯)) :
      ℝ≥0∞)
    (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ 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:
rw [dif_pos i.2]

Premises used: dif_pos, Subtype.property
-- 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)
ν : 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)
⊢ Measurable (α := (i : ι) → X i) (s.restrict (π := 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)
ν : 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)
⊢ Measurable (α := (i : ι) → X i) (s.restrict (π := X))

Tactic:
any_goals 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)
ν : 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) : ι)))
neg : ∀ (hi : i ∉ s), MeasurableSet.{u_2} (α := X i) Set.univ
⊢ MeasurableSet.{u_2} (α := X i) (if h : i ∈ s then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ s) i h) else Set.univ)

Tactic:
split_ifs with hi
-- 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)
ν : 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 : ι
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:
ht ⟨i, hi⟩

Premises used: Subtype.mk
-- 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)
ν : 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 : ι
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:
exact ht ⟨i, hi⟩

Premises used: Subtype.mk
-- 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)
ν : 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 : ι
hi : i ∉ s
⊢ MeasurableSet.{u_2} (α := X i) Set.univ

Tactic:
.univ

Premises used: MeasurableSet.univ
-- 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)
ν : 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 : ι
hi : i ∉ s
⊢ MeasurableSet.{u_2} (α := X i) Set.univ

Tactic:
exact .univ
-- 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)
ν : 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)
⊢ MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)

Tactic:
.univ_pi ht

Premises used: MeasurableSet.univ_pi
-- 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)
ν : 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)
⊢ MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)

Tactic:
exact .univ_pi ht
-- 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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
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
⊢ (↑s : Set ι).pi (α := X) t =
    cylinder (α := X) s (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))

Tactic:
ext x
-- 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 ι
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
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:
simp
-- 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 ι
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 : ι))

Tactic:
have : Set.pi s t = cylinder s ((@Set.univ s).pi (fun i : s ↦ t i)) := by
    ext x
    simp
-- 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 ι
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))
hs :
  MeasurableSet (α := (i : ↥s) → X (↑i : ι))
    (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∞)

Tactic:
rw [this, cylinder, ← map_apply, infinitePi_map_restrict, pi_pi]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.cylinder, MeasureTheory.Measure.infinitePi_map_restrict, MeasureTheory.Measure.pi_pi
-- 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 ι
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))
rw₁ rw₂ : Eq (α := ℝ≥0∞) (∏ x ∈ s, (μ x : (a : Set (X x)) → ℝ≥0∞) (t x)) (∏ 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))

Tactic:
rw [univ_eq_attach, prod_attach _ (fun i ↦ (μ i) (t i))]

Premises used: Finset.univ_eq_attach, Finset.prod_attach, DFunLike.coe
-- 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 ι
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 : ι))
⊢ Measurable (α := (i : ι) → X i) (s.restrict (π := X))

Tactic:
measurable_restrict _

Premises used: Finset.measurable_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 ι
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 : ι))
⊢ Measurable (α := (i : ι) → X i) (s.restrict (π := X))

Tactic:
exact measurable_restrict _

Premises used: Finset.measurable_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 ι
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 : ι))
⊢ MeasurableSet (α := (i : ↥s) → X (↑i : ι))
    (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))

Tactic:
.univ_pi fun i ↦ mt i.1 i.2

Premises used: Subtype.val, MeasurableSet.univ_pi, Subtype.property
-- 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 ι
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 : ι))
⊢ MeasurableSet (α := (i : ↥s) → X (↑i : ι))
    (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ fun (i : ↥s) ↦ t (↑i : ι))

Tactic:
exact .univ_pi fun i ↦ mt i.1 i.2
-- 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)
I : Set ι
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∞)
⊢ 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 : ι))

Tactic:
apply eq_infinitePi

Premises used: MeasureTheory.Measure.eq_infinitePi
-- 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)
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)
⊢ Measurable (α := (a : ι) → X a) (I.restrict (π := 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)
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)
⊢ ∀ i ∈ image (Subtype.val (p := fun (x : ι) ↦ x ∈ I)) s,
    MeasurableSet.{u_2} (α := X i) (if h : i ∈ I then t (Subtype.mk (p := fun (x : ι) ↦ x ∈ I) i h) else Set.univ)

Tactic:
measurability
-- 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)
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∞)
    (∏ 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:
simp
-- 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)
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)
⊢ ∀ i ∈ (↑s : Set (↑I : Type u_1)), MeasurableSet (t i)

Tactic:
measurability
-- 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)
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)
⊢ MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)

Tactic:
exact .pi s.countable_toSet (by measurability)
-- 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)
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)
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))
hν₅ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
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))
hν₇ : MeasurableSet ((↑s : Set (↑I : Type u_1)).pi (α := fun (i : (↑I : Type u_1)) ↦ X (↑i : ι)) t)
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))
hν₉ 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∞)

Tactic:
classical
  rw [map_apply (by fun_prop), restrict_preimage, infinitePi_pi _ (by measurability)]
  · simp
  · exact .pi s.countable_toSet (by measurability)

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.Measure.infinitePi_pi, Finset.restrict_preimage
-- 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 : Set ι
hs : Countable.{u_1 + 1} (↑s : Type u_1)
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
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∞)
wlog :
  ∀ {ι : 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∞)
⊢ 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

Premises used: Set.Elem, Nonempty