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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq (α := Set ((i : ι) → X i)) (⋂ (n : ℕ), A n) ∅
this : ∀ (i : ι), Nonempty.{u_2 + 1} (X i)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
⊢ Countable.{u_1 + 1} (↑u : Type u_1)

Tactic:
have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)
-- 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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq (α := Set ((i : ι) → X i)) (⋂ (n : ℕ), A n) ∅
this : ∀ (i : ι), Nonempty.{u_2 + 1} (X i)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
count_u : Countable.{u_1 + 1} (↑u : Type u_1)
φ : ℕ ≃ (↑u : Type u_1)
enter :
  fun (n : ℕ) ↦
    (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      (B n)
| Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n))
    atTop (𝓝 0)

Tactic:
enter [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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq (α := Set ((i : ι) → X i)) (⋂ (n : ℕ), A n) ∅
this : ∀ (i : ι), Nonempty.{u_2 + 1} (X i)
s : (n : ℕ) → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X (↑i : ι))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (s n) (S n)
u : Set ι := ⋃ (n : ℕ), (↑(s n) : Set ι)
t : (n : ℕ) → Finset (↑u : Type u_1) := fun (n : ℕ) ↦ (s n).preimage (Subtype.val (p := fun (x : ι) ↦ x ∈ u)) ⋯
f : ((i : (↑u : Type u_1)) → X (↑i : ι)) → (i : ι) → X i :=
  fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ι) ↦
    if hi : i ∈ u then x (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) i hi) else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun (n : ℕ) ↦
    { toFun := fun (i : ↥(t n)) ↦ Subtype.mk (p := fun (x : ι) ↦ x ∈ s n) (↑(↑i : (↑u : Type u_1)) : ι) ⋯,
      invFun := fun (i : ↥(s n)) ↦
        Subtype.mk (p := fun (x : (↑u : Type u_1)) ↦ x ∈ t n) (Subtype.mk (p := fun (x : ι) ↦ x ∈ u) (↑i : ι) ⋯) ⋯,
      left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) ≃ ((b : ↥(s n)) → X (↑b : ι)) :=
  fun (n : ℕ) ↦ Equiv.piCongrLeft.{u_2 + 1, u_1 + 1, u_1 + 1} (fun (i : ↥(s n)) ↦ X (↑i : ι)) (aux n)
r_comp_f :
  ∀ (n : ℕ),
    (s n).restrict (π := X) ∘ f =
      Function.comp (β := (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι))
        (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι))
        fun (x : (i : (↑u : Type u_1)) → X (↑i : ι)) (i : ↥(t n)) ↦ x (↑i : (↑u : Type u_1))
B : (n : ℕ) → Set ((i : (↑u : Type u_1)) → X (↑i : ι)) := fun (n : ℕ) ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) :=
  fun (n : ℕ) ↦
    (⇑(g n) : (a : (a : ↥(t n)) → X (↑((aux n : (a : ↥(t n)) → ↥(s n)) a) : ι)) → (b : ↥(s n)) → X (↑b : ι)) ⁻¹' S n
B_eq : ∀ (n : ℕ), B n = cylinder (α := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem :
  ∀ (n : ℕ),
    Membership.mem (γ := Set (Set ((i : (↑u : Type u_1)) → X (↑i : ι))))
      (measurableCylinders fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) (B n)
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : Eq (α := Set ((i : (↑u : Type u_1)) → X (↑i : ι))) (⋂ (n : ℕ), B n) ∅
u_inf : Infinite.{u_1 + 1} (↑u : Type u_1)
count_u : Countable.{u_1 + 1} (↑u : Type u_1)
φ : ℕ ≃ (↑u : Type u_1)
h :
  ∀ (n : ℕ),
    ((piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
          (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
        (B n) :
      ℝ≥0∞)
| fun (n : ℕ) ↦
    (piContent (X := fun (i : (↑u : Type u_1)) ↦ X (↑i : ι)) fun (i : (↑u : Type u_1)) ↦ μ (↑i : ι) :
        (a : Set ((i : (↑u : Type u_1)) → X (↑i : ι))) → ℝ≥0∞)
      (B n)

Tactic:
ext n
-- 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)
⊢ (piContent (X := X) μ).IsSigmaSubadditive (C := measurableCylinders X)

Tactic:
isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

Premises used: MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum, MeasureTheory.isSetRing_measurableCylinders
-- 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)
refine :
  ∀ (f : ℕ → Set ((i : ι) → X i)) (hf : ∀ (i : ℕ), f i ∈ measurableCylinders X)
    (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X) (hf' : Pairwise (Function.onFun Disjoint f)),
    Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
      (∑' (i : ℕ), (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)
⊢ (piContent (X := X) μ).IsSigmaSubadditive (C := measurableCylinders X)

Tactic:
refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)

Premises used: MeasureTheory.isSigmaSubadditive_of_addContent_iUnion_eq_tsum, MeasureTheory.isSetRing_measurableCylinders
-- 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)
f : ℕ → Set ((i : ι) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Function.onFun Disjoint f)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (piContent μ) (fun s hs ↦ projectiveFamilyContent_ne_top _)
    (fun _ ↦ piContent_tendsto_zero μ) hf hf_Union hf'

Premises used: MeasureTheory.piContent_tendsto_zero, MeasureTheory.piContent, MeasureTheory.isProjectiveMeasureFamily_pi, MeasureTheory.isSetRing_measurableCylinders, MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero, MeasureTheory.projectiveFamilyContent_ne_top
-- 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)
f : ℕ → Set ((i : ι) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Function.onFun Disjoint f)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)

Tactic:
exact addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (piContent μ) (fun s hs ↦ projectiveFamilyContent_ne_top _)
    (fun _ ↦ piContent_tendsto_zero μ) hf hf_Union hf'

Premises used: MeasureTheory.piContent_tendsto_zero, MeasureTheory.piContent, MeasureTheory.isProjectiveMeasureFamily_pi, MeasureTheory.isSetRing_measurableCylinders, MeasureTheory.addContent_iUnion_eq_sum_of_tendsto_zero, MeasureTheory.projectiveFamilyContent_ne_top
-- 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 : Finset ι
h :
  ∀ (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∞)
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ι))) (map (I.restrict (π := X)) (infinitePi (X := X) μ))
    ((fun (I : Finset ι) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι) : Measure ((i : ↥I) → X (↑i : ι))))
      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 : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
h : MeasurableSpace.pi (X := X) = MeasurableSpace.generateFrom (measurableCylinders X)
h₁ : I.restrict (π := X) ⁻¹' s ∈ 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∞)

Tactic:
rw [map_apply (measurable_restrict I) hs, infinitePi, dif_pos hμ, AddContent.measure_eq,
    ← cylinder, piContent_cylinder μ hs]

Premises used: MeasureTheory.AddContent.measure_eq, Finset.measurable_restrict, MeasureTheory.piContent_cylinder, MeasureTheory.Measure.map_apply, dif_pos, MeasureTheory.Measure.infinitePi, MeasureTheory.cylinder
-- 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 : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
⊢ MeasurableSpace.pi (X := X) = MeasurableSpace.generateFrom (measurableCylinders X)

Tactic:
generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, 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)
I : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
⊢ MeasurableSpace.pi (X := X) = MeasurableSpace.generateFrom (measurableCylinders X)

Tactic:
exact generateFrom_measurableCylinders.symm

Premises used: MeasureTheory.generateFrom_measurableCylinders, 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)
I : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
⊢ I.restrict (π := X) ⁻¹' s ∈ measurableCylinders X

Tactic:
cylinder_mem_measurableCylinders _ _ hs

Premises used: Set.Mem, MeasureTheory.cylinder, MeasureTheory.cylinder_mem_measurableCylinders
-- 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 : Finset ι
s : Set ((i : ↥I) → X (↑i : ι))
hs : MeasurableSet s
⊢ I.restrict (π := X) ⁻¹' s ∈ measurableCylinders X

Tactic:
exact cylinder_mem_measurableCylinders _ _ hs

Premises used: MeasureTheory.cylinder_mem_measurableCylinders
-- 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 : Finset ι
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ι))) (map (I.restrict (π := X)) (infinitePi (X := X) μ))
    (Measure.pi (α := fun (i : ↥I) ↦ X (↑i : ι)) fun (i : ↥I) ↦ μ (↑i : ι))

Tactic:
isProjectiveLimit_infinitePi μ I

Premises used: MeasureTheory.Measure.isProjectiveLimit_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)
measure_univ : Eq (α := ℝ≥0∞) ((infinitePi (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsProbabilityMeasure (infinitePi (X := X) μ)

Tactic:
constructor
-- 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_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∞)
measure_univ₄ measure_univ₅ : Eq (α := ℝ≥0∞) 1 1
⊢ Eq (α := ℝ≥0∞) ((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]

Premises used: Finset.measurable_restrict, MeasureTheory.Measure.map_apply, MeasureTheory.cylinder_univ, MeasureTheory.IsProbabilityMeasure.measure_univ, MeasureTheory.cylinder, MeasureTheory.Measure.infinitePi_map_restrict, EmptyCollection.emptyCollection, 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∞)
⊢ ν = infinitePi (X := X) μ

Tactic:
(isProjectiveLimit_infinitePi μ).unique ?_ |>.symm

Premises used: MeasureTheory.Measure.isProjectiveLimit_infinitePi, MeasureTheory.IsProjectiveLimit.unique, 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)
ν : 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∞)
refine :
  IsProjectiveLimit (α := X) ν fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)
⊢ ν = infinitePi (X := X) μ

Tactic:
refine (isProjectiveLimit_infinitePi μ).unique ?_ |>.symm

Premises used: MeasureTheory.Measure.isProjectiveLimit_infinitePi, MeasureTheory.IsProjectiveLimit.unique, 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)
ν : 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 : ι)

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

Premises used: MeasureTheory.IsProjectiveLimit, 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)
ν : 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∞)
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∞)
⊢ IsProjectiveLimit (α := X) ν fun (I : Finset ι) ↦
    Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ι)) fun (i : ↥I) ↦ μ (↑i : ι)

Tactic:
refine fun s ↦ (pi_eq fun t ht ↦ ?_).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)
ν : 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))
hs : MeasurableSet (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t)
⊢ Eq (α := ℝ≥0∞)
    ((map (s.restrict (π := X)) ν : (a : Set ((i : ↥s) → X (↑i : ι))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥s) ↦ X (↑i : ι)) Set.univ t) :
      ℝ≥0∞)
    (∏ i : ↥s, ((μ (↑i : ι) : Measure (X (↑i : ι))) : (a : Set (X (↑i : ι))) → ℝ≥0∞) (t i) : ℝ≥0∞)

Tactic:
rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]

Premises used: MeasureTheory.Measure.map_apply, Finset.restrict_preimage_univ, Finset.univ_eq_attach, Finset.prod_attach