awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
⊢ Ne (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑{s_ne.some} : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
          if i ∈ s then t i else Set.univ) :
      ℝ≥0∞)
    (∞ : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
this :
  s.pi (α := X) t =
    ⋂ (s' : Finset (↑s : Type u_1)),
      (Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑s' : Set (↑s : Type u_1))).pi (α := X) fun (i : ι) ↦
        if i ∈ s then t i else Set.univ
⊢ ∃ (i : Finset (↑s : Type u_1)),
    Ne (α := ℝ≥0∞)
      ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
          ((Subtype.val (p := fun (x : ι) ↦ x ∈ s) '' (↑i : Set { x : ι // x ∈ s })).pi (α := X) fun (i : ι) ↦
            if i ∈ s then t i else Set.univ) :
        ℝ≥0∞)
      (∞ : ℝ≥0∞)

Tactic:
exact ⟨{Nonempty.some s_ne}, by simp⟩
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
⊢ ∀ (i : (↑s : Type u_1)),
    LE.le (α := ℝ≥0∞) (((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)) : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
simp [prob_le_one]

Premises used: MeasureTheory.prob_le_one
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
hb :
  Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    atTop
    (𝓝
      (⨅ (s_1 : Finset (↑s : Type u_1)),
        ∏ i ∈ s_1, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    atTop
    (𝓝 (∏' (i : (↑s : Type u_1)), ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))

Tactic:
rw [ENNReal.tprod_eq_iInf_prod (by simp [prob_le_one])]

Premises used: ENNReal.tprod_eq_iInf_prod
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
⊢ ∀ (x : (↑s : Type u_1)),
    LE.le (α := ℝ≥0∞) (((μ (↑x : ι) : Measure (X (↑x : ι))) : (a : Set (X (↑x : ι))) → ℝ≥0∞) (t (↑x : ι)) : ℝ≥0∞)
      (1 : ℝ≥0∞)

Tactic:
simp [prob_le_one]

Premises used: MeasureTheory.prob_le_one
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι_1 : Type u_1
X_1 : ι_1 → Type u_2
mX_1 : (i : ι_1) → MeasurableSpace (X_1 i)
μ_1 : (i : ι_1) → Measure (X_1 i)
ι : 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)
⊢ Tendsto (β := ℝ≥0∞)
    (fun (s' : Finset (↑s : Type u_1)) ↦
      ∏ i ∈ s', ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι)))
    atTop
    (𝓝
      (⨅ (s_1 : Finset (↑s : Type u_1)),
        ∏ i ∈ s_1, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t (↑i : ι))))

Tactic:
exact tendsto_atTop_iInf (prod_anti_set_of_le_one' (by simp [prob_le_one]))

Premises used: Finset.prod_anti_set_of_le_one', tendsto_atTop_iInf
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
hs : Countable.{u_1 + 1} (↑Set.univ : Type u_1)
mt₁ : ∀ (i : ι), Membership.mem (γ := Set ι) Set.univ i → MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ t) : ℝ≥0∞)
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
rw [infinitePi_pi_of_countable, tprod_univ (f := fun i ↦ μ i (t i))]

Premises used: tprod_univ, DFunLike.coe, MeasureTheory.Measure.infinitePi_pi_of_countable
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ Countable.{u_1 + 1} (↑Set.univ : Type u_1)

Tactic:
simpa [Set.countable_univ_iff]

Premises used: Set.countable_univ_iff
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst : Countable ι
t : (i : ι) → Set (X i)
mt : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (i : ι), Membership.mem (γ := Set ι) Set.univ i → 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)
inst : Countable ι
inst_1 : ∀ (i : ι), MeasurableSingletonClass.{u_2} (X i)
f : (i : ι) → X i
⊢ ∀ (i : ι), MeasurableSet (α := X i) {f 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)
inst : Countable ι
inst_1 : ∀ (i : ι), MeasurableSingletonClass.{u_2} (X i)
f : (i : ι) → X i
rw :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ fun (i : ι) ↦ {f i}) : ℝ≥0∞)
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i} : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i}) (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) {f})
    (∏' (i : ι), (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})

Tactic:
rw [← Set.univ_pi_singleton, infinitePi_pi_univ _ (by measurability)]

Premises used: Set.univ_pi_singleton, MeasureTheory.Measure.infinitePi_pi_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)
inst : Fintype ι
inst_1 : ∀ (i : ι), MeasurableSingletonClass.{u_2} (X i)
f : (i : ι) → X i
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) {f})
    (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) {f i})

Tactic:
simp
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
f : (i : ι) → X i
⊢ ∀ (s : Finset ι) (t : (i : ι) → Set (X i)),
    (∀ (i : ι), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞) ((dirac f : (a : Set ((i : ι) → X i)) → ℝ≥0∞) ((↑s : Set ι).pi (α := X) t) : ℝ≥0∞)
        (∏ i ∈ s, ((dirac (f i) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
simp +contextual [MeasurableSet.pi, Finset.countable_toSet]

Premises used: Finset.countable_toSet, MeasurableSet.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)
i : ι
⊢ Measurable (α := (x : ι) → X x) (Function.eval (β := X) i)

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 : ι
h :
  ∀ (s : Set (X i)) (hs : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
      ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
⊢ map (Function.eval (β := X) i) (infinitePi (X := X) μ) = μ i

Tactic:
ext s hs
-- 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 : ι
s : Set (X i)
hs : MeasurableSet s
⊢ Membership.mem (γ := Finset ι) {i} 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 : ι
s : Set (X i)
hs : MeasurableSet s
h :
  ∀ (x : (x : ι) → X x),
    Function.eval (β := X) i x =
      Function.comp (β := (x : ↥{i}) → X (↑x : ι))
        (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
          (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
        (Finset.restrict (π := X) {i}) x
⊢ Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))

Tactic:
ext
-- 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 : ι
s : Set (X i)
hs : MeasurableSet s
x : (x : ι) → X x
⊢ Function.eval (β := X) i x =
    Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {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)
i : ι
s : Set (X i)
hs : MeasurableSet s
⊢ Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))

Tactic:
have : @Function.eval ι X i =
        (@Function.eval ({i} : Finset ι) (fun j ↦ X j) ⟨i, by simp⟩) ∘
        (Finset.restrict {i}) := by ext; 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 : ι
s : Set (X i)
hs : MeasurableSet s
this :
  Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
h :
  Measurable (α := (x : ↥{i}) → X (↑x : ι))
    (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
h₁ : Measurable (α := (x : ι) → X x) (β := (x : ↥{i}) → X (↑x : ι)) (Finset.restrict (π := X) {i})
⊢ Eq (α := ℝ≥0∞)
    (((map (Function.eval (β := X) i) (infinitePi (X := X) μ) : Measure (X i)) : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]

Premises used: MeasureTheory.measurePreserving_eval, MeasureTheory.MeasurePreserving.map_eq, MeasureTheory.Measure.infinitePi_map_restrict, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
i : ι
s : Set (X i)
hs : MeasurableSet s
this :
  Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
⊢ Measurable (α := (x : ↥{i}) → X (↑x : ι))
    (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
      (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))

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 : ι
s : Set (X i)
hs : MeasurableSet s
this :
  Eq (α := (f : (x : ι) → X x) → X i) (Function.eval (β := X) i)
    (Function.comp (β := (x : ↥{i}) → X (↑x : ι))
      (Function.eval (β := fun (j : ↥{i}) ↦ X (↑j : ι))
        (Subtype.mk (p := fun (x : ι) ↦ Membership.mem (γ := Finset ι) {i} x) i ⋯))
      (Finset.restrict (π := X) {i}))
⊢ Measurable (α := (x : ι) → X x) (β := (x : ↥{i}) → X (↑x : ι)) (Finset.restrict (π := X) {i})

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 : ι
⊢ map (fun (x : (i : ι) → X i) ↦ x i) (infinitePi (X := X) μ) = μ i

Tactic:
(measurePreserving_eval_infinitePi μ i).map_eq

Premises used: MeasureTheory.MeasurePreserving.map_eq, measurePreserving_eval_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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
⊢ ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))

Tactic:
have (i : ι) : IsProbabilityMeasure ((μ i).map (f i)) :=
    isProbabilityMeasure_map (hf i).aemeasurable
-- 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ))
    (infinitePi (X := Y) fun (i : ι) ↦ map (f i) (μ i))

Tactic:
eq_infinitePi _ fun s t ht ↦ ?_

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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
refine :
  ∀ (s : Finset ι) (t : (i : ι) → Set (Y i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
    Eq (α := ℝ≥0∞)
      ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
          ((↑s : Set ι).pi (α := Y) t) :
        ℝ≥0∞)
      (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ Eq (α := Measure ((i : ι) → Y i)) (map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ))
    (infinitePi (X := Y) fun (i : ι) ↦ map (f i) (μ i))

Tactic:
refine eq_infinitePi _ fun s t ht ↦ ?_

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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable (β := (i : ι) → Y i) fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)

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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
rw :
  Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i))
          ((↑s : Set ι).pi (α := fun (i : ι) ↦ Y i) fun (x : ι) ↦ t x)) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) (infinitePi (X := X) μ) : (a : Set ((i : ι) → Y i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := Y) t) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) (.pi s.countable_toSet fun _ _ ↦ ht _)]

Premises used: MeasureTheory.Measure.map_apply, Finset.countable_toSet, MeasurableSet.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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
h :
  ∀ (x : (i : ι) → X i),
    Membership.mem (γ := Set ((i : ι) → X i))
        ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t) x ↔
      Membership.mem (γ := Set ((i : ι) → X i)) ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i) x
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
x : (i : ι) → X i
⊢ Membership.mem (γ := Set ((i : ι) → X i))
      ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t) x ↔
    Membership.mem (γ := Set ((i : ι) → X i)) ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' 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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)

Tactic:
have : (fun (x : Π i, X i) i ↦ f i (x i)) ⁻¹' ((s : Set ι).pi t) =
      (s : Set ι).pi (fun i ↦ (f i) ⁻¹' (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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this_1 : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
rw :
  Eq (α := ℝ≥0∞) (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i))
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i))
⊢ Eq (α := ℝ≥0∞)
    ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.preimage (β := (i : ι) → Y i) (fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i))
          ((↑s : Set ι).pi (α := fun (i : ι) ↦ Y i) fun (x : ι) ↦ t x)) :
      ℝ≥0∞)
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
rw [this, infinitePi_pi _ (fun i _ ↦ hf i (ht i))]

Premises used: MeasureTheory.Measure.infinitePi_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)
Y : ι → Type u_3
inst : (i : ι) → MeasurableSpace (Y i)
f : (i : ι) → X i → Y i
hf : ∀ (i : ι), Measurable (f i)
this_1 : ∀ (i : ι), IsProbabilityMeasure (m0 := inst i) (map (f i) (μ i))
s : Finset ι
t : (i : ι) → Set (Y i)
ht : ∀ (i : ι), MeasurableSet (t i)
this :
  Eq (α := Set ((i : ι) → X i)) ((fun (x : (i : ι) → X i) (i : ι) ↦ f i (x i)) ⁻¹' (↑s : Set ι).pi (α := Y) t)
    ((↑s : Set ι).pi (α := X) fun (i : ι) ↦ f i ⁻¹' t i)
a :
  ∀ (i : ι) (hi : i ∈ s),
    Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
      (((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i))
    (∏ i ∈ s, ((map (f i) (μ i) : Measure (Y i)) : (a : Set (Y i)) → ℝ≥0∞) (t i))

Tactic:
congr! with i hi