awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
⊢ n ≤ n + 1

Tactic:
lia
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ IsEmpty ↥(Ioc a b)

Tactic:
simpa [hba] using Subtype.isEmpty_false

Premises used: Subtype.isEmpty_false
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ IsEmpty ↥(Ioc a b)

Tactic:
have : IsEmpty (Ioc a b) := by simpa [hba] using Subtype.isEmpty_false
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
inr :
  ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)) (s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                    (restrict₂ (π := X) ⋯) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                    (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))

Tactic:
ext x s ms
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
pos :
  ∀ (hs : s.Nonempty),
    Eq (α := ℝ≥0∞)
      ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                    (restrict₂ (π := X) ⋯) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                    (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
neg :
  ∀ (hs : ¬s.Nonempty),
    Eq (α := ℝ≥0∞)
      ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                    (restrict₂ (π := X) ⋯) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                    (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                  (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
by_cases hs : s.Nonempty

Premises used: Set.Nonempty
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : s.Nonempty
rw :
  IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
          (restrict₂ (π := X) ⋯) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      x)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Subsingleton.eq_univ_of_nonempty hs, @measure_univ .., measure_univ]

Premises used: MeasureTheory.IsProbabilityMeasure.measure_univ, Subsingleton.eq_univ_of_nonempty
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : s.Nonempty
⊢ IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
          (restrict₂ (π := X) ⋯) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      x)

Tactic:
(IsMarkovKernel.map _ (measurable_restrict₂ _)) |>.isProbabilityMeasure x

Premises used: ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : s.Nonempty
⊢ IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
          (restrict₂ (π := X) ⋯) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      x)

Tactic:
exact (IsMarkovKernel.map _ (measurable_restrict₂ _)) |>.isProbabilityMeasure x

Premises used: ProbabilityTheory.IsMarkovKernel.isProbabilityMeasure
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : ¬s.Nonempty
neg :
  Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        ∅ :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        ∅ :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
rw [Set.not_nonempty_iff_eq_empty.1 hs]

Premises used: Set.not_nonempty_iff_eq_empty, Iff.mp
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
hs : ¬s.Nonempty
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        ∅ :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        ∅ :
      ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
rw :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
          (restrict₂ (π := X) ⋯))
      (_root_.IicProdIoc (X := X) a b))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
    (Kernel.map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ
        const ((i : ↥(Iic a)) → X (↑i : ℕ))
          (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b))

Tactic:
rw [partialTraj_eq_prod, partialTraj_const_restrict₂]

Premises used: MeasureTheory.partialTraj_const_restrict₂, ProbabilityTheory.Kernel.partialTraj_eq_prod
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) 0 (I.sup id))
hf₁ :
  Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ))
    (frestrictLe (π := X) (I.sup id))
hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
hf₂ : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (I.sup id)).restrict (π := X))
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    ((fun (I : Finset ℕ) ↦
        (Measure.pi (α := fun (j : ↥I) ↦ X (↑j : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ) : Measure ((i : ↥I) → X (↑i : ℕ))))
      I)

Tactic:
rw [isProjectiveMeasureFamily_pi μ _ _ I.subset_Iic_sup_id,
    ← restrict₂_comp_restrict I.subset_Iic_sup_id, ← map_map, ← frestrictLe, infinitePiNat,
    map_comp, traj_map_frestrictLe, partialTraj_const, ← map_comp, ← compProd_eq_comp_prod,
    compProd_const, pi_prod_map_IicProdIoc]

Premises used: MeasureTheory.Measure.map_comp, MeasureTheory.isProjectiveMeasureFamily_pi, MeasureTheory.Measure.pi_prod_map_IicProdIoc, MeasureTheory.partialTraj_const, Finset.restrict₂_comp_restrict, MeasureTheory.Measure.compProd_eq_comp_prod, MeasureTheory.Measure.infinitePiNat, ProbabilityTheory.Kernel.traj_map_frestrictLe, Preorder.frestrictLe, Finset.subset_Iic_sup_id, MeasureTheory.Measure.map_map, MeasureTheory.Measure.compProd_const
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic 0)) → X (↑i : ℕ)) × ((i : ↥(Ioc 0 (I.sup id))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) 0 (I.sup id))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) (β := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ))
    (frestrictLe (π := X) (I.sup id))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (I.sup id)).restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ Eq (α := Measure ((i : ↥I) → X (↑i : ℕ))) (map (I.restrict (π := X)) (infinitePiNat (X := X) μ))
    (Measure.pi (α := fun (i : ↥I) ↦ X (↑i : ℕ)) fun (i : ↥I) ↦ μ (↑i : ℕ))

Tactic:
isProjectiveLimit_infinitePiNat μ I

Premises used: MeasureTheory.Measure.isProjectiveLimit_infinitePiNat
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
A : Set ((n : ℕ) → X n)
hA : A ∈ measurableCylinders X
⊢ ∃ (s : Finset ℕ) (S : Set ((i : ↥s) → X (↑i : ℕ))), MeasurableSet S ∧ A = cylinder (α := X) s S

Tactic:
simpa [mem_measurableCylinders] using hA

Premises used: MeasureTheory.mem_measurableCylinders
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
A : Set ((n : ℕ) → X n)
hA : A ∈ measurableCylinders X
obtain :
  ∀ (s : Finset ℕ) (S : Set ((i : ↥s) → X (↑i : ℕ))) (mS : MeasurableSet S)
    (hA : cylinder (α := X) s S ∈ measurableCylinders X),
    Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
      ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) A : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) A : ℝ≥0∞)

Tactic:
obtain ⟨s, S, mS, rfl⟩ : ∃ s S, MeasurableSet S ∧ A = cylinder s S := by
    simpa [mem_measurableCylinders] using hA

Premises used: rfl
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
s : Finset ℕ
S : Set ((i : ↥s) → X (↑i : ℕ))
mS : MeasurableSet S
hA : cylinder (α := X) s S ∈ measurableCylinders X
rw :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (s.restrict (π := X) ⁻¹' S) : ℝ≥0∞)
rw₂ :
  Eq (α := ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    (((map (s.restrict (π := X)) (infinitePiNat (X := X) μ) : Measure ((i : ↥s) → X (↑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 : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    (((Measure.pi (α := fun (i : ↥s) ↦ X (↑i : ℕ)) fun (i : ↥s) ↦ μ (↑i : ℕ) : Measure ((i : ↥s) → X (↑i : ℕ))) :
          (a : Set ((i : ↥s) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((piContent (X := X) μ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)
    ((infinitePiNat (X := X) μ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) (cylinder (α := X) s S) : ℝ≥0∞)

Tactic:
rw [piContent_cylinder _ mS, cylinder, ← map_apply (measurable_restrict _) mS,
    infinitePiNat_map_restrict]

Premises used: Finset.measurable_restrict, MeasureTheory.piContent_cylinder, MeasureTheory.Measure.map_apply, MeasureTheory.cylinder, MeasureTheory.Measure.infinitePiNat_map_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)
e : ℕ ≃ ι
s : Set ((i : ι) → X i)
hs : s ∈ measurableCylinders X
obtain :
  ∀ (I : Finset ι) (S : Set ((i : ↥I) → X (↑i : ι))) (hS : MeasurableSet S)
    (hs : cylinder (α := X) I S ∈ measurableCylinders X),
    Eq (α := ℝ≥0∞)
      ((map (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b))
              (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
              (infinitePiNat (X := fun (n : ℕ) ↦ X ((e : (a : ℕ) → ι) n)) fun (n : ℕ) ↦ μ ((e : (a : ℕ) → ι) n)) :
            (a : Set ((a : ι) → X a)) → ℝ≥0∞)
          (cylinder (α := X) I S) :
        ℝ≥0∞)
      ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) (cylinder (α := X) I S) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞)
    ((map (α := (b : ℕ) → X ((e : (a : ℕ) → ι) b))
            (⇑(piCongrLeft X e) : (a : (b : ℕ) → X ((e : (a : ℕ) → ι) b)) → (a : ι) → X a)
            (infinitePiNat (X := fun (n : ℕ) ↦ X ((e : (a : ℕ) → ι) n)) fun (n : ℕ) ↦ μ ((e : (a : ℕ) → ι) n)) :
          (a : Set ((a : ι) → X a)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((piContent (X := X) μ : (a : Set ((i : ι) → X i)) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
obtain ⟨I, S, hS, rfl⟩ := (mem_measurableCylinders s).1 hs

Premises used: Iff.mp, MeasureTheory.mem_measurableCylinders, rfl