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)
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)
i : ι
hi : i ∈ s
⊢ Measurable (f 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_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)
i : ι
hi : i ∈ s
a a₁ :
  Eq (α := ℝ≥0∞) ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
    ((μ i : (a : Set (X i)) → ℝ≥0∞) (f i ⁻¹' t i) : ℝ≥0∞)
⊢ 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∞)

Tactic:
rw [map_apply (by fun_prop) (ht i)]

Premises used: MeasureTheory.Measure.map_apply
-- 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)
α : Type u_3
e : α ≃ ι
⊢ map (α := (b : α) → X ((e : (a : α) → ι) b))
      (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
      (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) =
    infinitePi (X := X) μ

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)
α : Type u_3
e : α ≃ ι
refine :
  ∀ (s : Finset ι) (t : (i : ι) → Set (X i)) (ht : ∀ (i : ι), MeasurableSet (t i)),
    Eq (α := ℝ≥0∞)
      ((map (α := (b : α) → X ((e : (a : α) → ι) b))
              (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
              (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
            (a : Set ((i : ι) → X i)) → ℝ≥0∞)
          ((↑s : Set ι).pi (α := X) t) :
        ℝ≥0∞)
      (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ map (α := (b : α) → X ((e : (a : α) → ι) b))
      (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
      (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) =
    infinitePi (X := X) μ

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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
enter : (↑s : Set ι)
| ((map (α := (b : α) → X ((e : (a : α) → ι) b))
          (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
          (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((↑s : Set ι).pi (α := X) t) :
    ℝ≥0∞)

Tactic:
enter [2, 1]
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
rw : (⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)
| (↑s : Set ι)

Tactic:
rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]

Premises used: Function.Injective.injOn, Finset.coe_preimage, SetLike.coe, Equiv.injective, Equiv.image_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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
enter : (⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)
| ((map (α := (b : α) → X ((e : (a : α) → ι) b))
          (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
          (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
        (a : Set ((i : ι) → X i)) → ℝ≥0∞)
      ((↑s : Set ι).pi (α := X) t) :
    ℝ≥0∞)

Tactic:
enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]

Premises used: Function.Injective.injOn, Finset.coe_preimage, SetLike.coe, Equiv.injective, Equiv.image_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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
conv_lhs :
  Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        ((↑s : Set ι).pi (α := X) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
conv_lhs => enter [2, 1]; rw [← e.image_preimage s, ← coe_preimage _ e.injective.injOn]

Premises used: Function.Injective.injOn, Finset.coe_preimage, SetLike.coe, Equiv.injective, Equiv.image_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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
hst : ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) i : ι)
hfg :
  ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯,
    Eq (α := ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
mt : ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯, MeasurableSet (α := X ((e : (a : α) → ι) i)) (t ((e : (a : α) → ι) i))
hf :
  Measurable (α := (b : α) → X ((e : (a : α) → ι) b)) (β := (a : ι) → X a)
    (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
hs : MeasurableSet (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : α) → X ((e : (a : α) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)
            (infinitePi (X := fun (i : α) ↦ X ((e : (a : α) → ι) i)) fun (i : α) ↦ μ ((e : (a : α) → ι) i)) :
          (a : Set ((i : ι) → X i)) → ℝ≥0∞)
        (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t) :
      ℝ≥0∞)
    (∏ i ∈ s, (μ i : (a : Set (X i)) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
rw [map_apply, coe_piCongrLeft, Equiv.piCongrLeft_preimage_pi, infinitePi_pi,
    prod_equiv e]

Premises used: MeasureTheory.Measure.map_apply, Equiv.piCongrLeft_preimage_pi, MeasureTheory.Measure.infinitePi_pi, Finset.prod_equiv, MeasurableEquiv.coe_piCongrLeft
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (i : α), i ∈ s.preimage (⇑e : (a : α) → ι) ⋯ ↔ Membership.mem (α := ι) s ((e : (a : α) → ι) 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯,
    Eq (α := ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)
      (((μ ((e : (a : α) → ι) i) : Measure (X ((e : (a : α) → ι) i))) : (a : Set (X ((e : (a : α) → ι) i))) → ℝ≥0∞)
          (t ((e : (a : α) → ι) i)) :
        ℝ≥0∞)

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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ i ∈ s.preimage (⇑e : (a : α) → ι) ⋯, MeasurableSet (α := X ((e : (a : α) → ι) i)) (t ((e : (a : α) → ι) i))

Tactic:
simp_all
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ Measurable (α := (b : α) → X ((e : (a : α) → ι) b)) (β := (a : ι) → X a)
    (⇑(piCongrLeft X e) : (a : (b : α) → X ((e : (a : α) → ι) b)) → (a : ι) → X a)

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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ ∀ (i : ι),
    Membership.mem (γ := Set ι) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) i →
      MeasurableSet (t i)

Tactic:
simp_all
-- 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)
α : Type u_3
e : α ≃ ι
s : Finset ι
t : (i : ι) → Set (X i)
ht : ∀ (i : ι), MeasurableSet (t i)
⊢ MeasurableSet (Set.pi (α := X) ((⇑e : (a : α) → ι) '' (↑(s.preimage (⇑e : (a : α) → ι) ⋯) : Set α)) t)

Tactic:
exact .pi ((countable_toSet _).image e) (by simp_all)
-- 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 ι
⊢ infinitePi (X := X) μ = Measure.pi (α := X) μ

Tactic:
(pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- 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 ι
refine :
  ∀ (s : (i : ι) → Set (X i)) (hs : ∀ (i : ι), MeasurableSet (s i)),
    Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ s) : ℝ≥0∞)
      (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)
⊢ infinitePi (X := X) μ = Measure.pi (α := X) μ

Tactic:
refine (pi_eq fun s hs ↦ ?_).symm

Premises used: MeasureTheory.Measure.pi_eq, Eq.symm
-- 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 ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
mt : ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (Set.pi (α := X) Set.univ s) : ℝ≥0∞)
    (∏ i : ι, (μ i : (a : Set (X i)) → ℝ≥0∞) (s i) : ℝ≥0∞)

Tactic:
rw [← coe_univ, infinitePi_pi]

Premises used: Finset.coe_univ, 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)
inst : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ (i : ι), Membership.mem (γ := Finset ι) univ i → MeasurableSet (s i)

Tactic:
simpa
-- 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 ι
S : Set ((i : ↥s) → X (↑i : ι))
mS : MeasurableSet S
rw :
  Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) (infinitePi (X := X) μ) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞) S : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) fun (i : ↥s) ↦ μ (↑i : ι) : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        S :
      ℝ≥0∞)

Tactic:
rw [cylinder, ← Measure.map_apply (measurable_restrict _) mS, infinitePi_map_restrict]

Premises used: Finset.measurable_restrict, MeasureTheory.Measure.map_apply, MeasureTheory.cylinder, MeasureTheory.Measure.infinitePi_map_restrict
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
hν :
  ∀ (s : Finset ((i : ι) × κ i))
    (t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))),
    (∀ (i : (i : ι) × κ i), MeasurableSet (t i)) →
      Eq (α := ℝ≥0∞)
        ((map (α := (i : ι) → (j : κ i) → X i j)
                (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
                  (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
                (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦
                  infinitePi (X := X i) fun (j : κ i) ↦ μ i j) :
              (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
            ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
              X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
          ℝ≥0∞)
        (∏ i ∈ s,
            (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞)
              (t i) :
          ℝ≥0∞)
⊢ Eq (α := Measure ((p : (i : ι) × κ i) → X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i))))
    (map (α := (i : ι) → (j : κ i) → X i j)
      (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
        (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
      (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦ infinitePi (X := X i) fun (j : κ i) ↦ μ i j))
    (infinitePi (X := fun (p : (i : ι) × κ i) ↦ X (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))
      fun (p : (i : ι) × κ i) ↦ μ (p.fst (β := fun (i : ι) ↦ κ i)) (p.snd (β := fun (i : ι) ↦ κ i)))

Tactic:
apply eq_infinitePi

Premises used: MeasureTheory.Measure.eq_infinitePi
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ Measurable (α := (i : ι) → (j : κ i) → X i j) (β :=
    (i : (i : ι) × κ i) → X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
    (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
      (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
hν :
  Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))
hν₁ :
  ∀ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
    MeasurableSet (α := (i_1 : κ i) → X i i_1)
      ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
        X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
          ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
        fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j))
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (i : ι) → (j : κ i) → X i j)
            (⇑(MeasurableEquiv.symm (piCurry (κ := κ) X)) :
              (a : (i : ι) → (j : κ i) → X i j) → (p : (i : ι) × κ i) → X p.fst p.snd)
            (infinitePi (X := fun (i : ι) ↦ (i_1 : κ i) → X i i_1) fun (i : ι) ↦
              infinitePi (X := X i) fun (j : κ i) ↦ μ i j) :
          (a : Set ((i : (i : ι) × κ i) → X i.fst i.snd)) → ℝ≥0∞)
        ((↑s : Set ((i : ι) × κ i)).pi (α := fun (i : (i : ι) × κ i) ↦
          X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i))) t) :
      ℝ≥0∞)
    (∏ i ∈ s,
        (μ (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)) : (a : Set (X i.fst i.snd)) → ℝ≥0∞) (t i) :
      ℝ≥0∞)

Tactic:
rw [map_apply (by fun_prop) (.pi (countable_toSet _) fun _ _ ↦ ht _),
    ← Finset.sigma_image_fst_preimage_mk s, coe_piCurry_symm, Finset.coe_sigma,
    Set.uncurry_preimage_sigma_pi, infinitePi_pi, Finset.prod_sigma]

Premises used: Finset.sigma_image_fst_preimage_mk, MeasureTheory.Measure.map_apply, MeasureTheory.Measure.infinitePi_pi, Finset.prod_sigma, Finset.countable_toSet, Set.uncurry_preimage_sigma_pi, MeasurableEquiv.coe_piCurry_symm, Finset.coe_sigma, MeasurableSet.pi
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))

Tactic:
Finset.prod_congr rfl (fun _ _ ↦ infinitePi_pi _ fun _ _ ↦ ht _)

Premises used: MeasureTheory.Measure.infinitePi_pi, Finset.prod_congr, Sigma.mk, rfl
-- Module: Mathlib.Probability.ProductMeasure
Goal:
ι : Type u_3
κ : ι → Type u_4
X : (i : ι) → κ i → Type u_5
mX : (i : ι) → (j : κ i) → MeasurableSpace (X i j)
μ : (i : ι) → (j : κ i) → Measure (X i j)
hμ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (μ i j)
s : Finset ((i : ι) × κ i)
t : (i : (i : ι) × κ i) → Set (X (i.fst (β := fun (i : ι) ↦ κ i)) (i.snd (β := fun (i : ι) ↦ κ i)))
ht : ∀ (i : (i : ι) × κ i), MeasurableSet (t i)
⊢ Eq (α := ℝ≥0∞)
    (∏ i ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      (infinitePi (X := X i) fun (j : κ i) ↦ μ i j : (a : Set ((i_1 : κ i) → X i i_1)) → ℝ≥0∞)
        ((↑(s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) i) ⋯) : Set (κ i)).pi (α := fun (j : κ i) ↦
          X ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).fst (β := fun (i : ι) ↦ κ i))
            ((Sigma.mk (β := fun (i : ι) ↦ κ i) i j).snd (β := fun (i : ι) ↦ κ i)))
          fun (j : κ i) ↦ t (Sigma.mk (β := fun (i : ι) ↦ κ i) i j)))
    (∏ a ∈ image (Sigma.fst (β := fun (a : ι) ↦ κ a)) s,
      ∏ s ∈ s.preimage (Sigma.mk (β := fun (a : ι) ↦ κ a) a) ⋯,
        (μ ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).fst (β := fun (i : ι) ↦ κ i))
              ((Sigma.mk (β := fun (a : ι) ↦ κ a) a s).snd (β := fun (i : ι) ↦ κ i)) :
            (a : Set (X ⟨a, s⟩.fst ⟨a, s⟩.snd)) → ℝ≥0∞)
          (t (Sigma.mk (β := fun (a : ι) ↦ κ a) a s)))

Tactic:
exact Finset.prod_congr rfl (fun _ _ ↦ infinitePi_pi _ fun _ _ ↦ ht _)

Premises used: MeasureTheory.Measure.infinitePi_pi, Finset.prod_congr, rfl