awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq.{u_1 + 1} (α := Set ((n : ℕ) → X n)) (⋂ (n : ℕ), A n) ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X (↑i : ℕ)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
a : (n : ℕ) → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X (↑i : ℕ))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (Iic (a n)) (S n)
χ : (n : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv :
  ∀ (k M n : ℕ) (h : a n ≤ M), lmarginalPartialTraj (X := X) κ k M (χ n) = lmarginalPartialTraj (X := X) κ k (a n) (χ n)
anti_lma :
  ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
l : (k : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞
hl :
  ∀ (k : ℕ) (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = ε
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → (y : (i : ↥(Iic k)) → X (↑i : ℕ)) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X (↑i : ℕ))
    (h :
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) y))
    (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤
      lmarginalPartialTraj (X := X) κ (k + 1) (a n) (χ n)
        (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction (X := X) x₀ ind
main :
  ∀ (k : ℕ) (hk : p ≤ k) (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) (frestrictLe (π := X) k z))
aux :
  ∀ (x : (i : ℕ) → X i) (n : ℕ),
    (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (A n) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
this : 0 ≠ ε
⊢ False
have mem : ∀ (n : ℕ), z ∈ A n
Tactic: have mem n : z ∈ A n := by
    have : 0 < χ n z := by
      rw [← lmarginalPartialTraj_le κ (le_max_right p (a n)) (mχ n),
        ← updateFinset_frestrictLe (a := a n) z]
      simpa using lt_of_lt_of_le this.symm.bot_lt (main _ (le_max_left _ _) z n)
    exact Set.mem_of_indicator_ne_zero (ne_of_lt this).symm
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ (trajContent (X := X) κ x₀).IsSigmaSubadditive (C := measurableCylinders X)
have refine : ∀ (f : ℕ → Set ((i : ℕ) → X i)) (hf : ∀ (i : ℕ), f i ∈ measurableCylinders X)
  (hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X) (hf' : Pairwise (Disjoint on f)),
  Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)
Tactic: refine isSigmaSubadditive_of_addContent_iUnion_eq_tsum
    isSetRing_measurableCylinders (fun f hf hf_Union hf' ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ℕ → Set ((i : ℕ) → X i)
hf : ∀ (i : ℕ), f i ∈ measurableCylinders X
hf_Union : ⋃ (i : ℕ), f i ∈ measurableCylinders X
hf' : Pairwise (Disjoint on f)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
    (∑' (i : ℕ), (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (f i) : ℝ≥0∞)
have refine : ∀ ⦃s : ℕ → Set ((i : ℕ) → X i)⦄,
  (∀ (n : ℕ), s n ∈ measurableCylinders X) →
    Antitone s →
      Eq.{u_1 + 1} (α := Set ((i : ℕ) → X i)) (⋂ (n : ℕ), s n) ∅ →
        Tendsto (β := ℝ≥0∞) (fun (n : ℕ) ↦ (trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (s n)) atTop
          (𝓝 0)
Tactic: refine addContent_iUnion_eq_sum_of_tendsto_zero isSetRing_measurableCylinders
    (trajContent κ x₀) (fun _ _ ↦ trajContent_ne_top) ?_ hf hf_Union hf'
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq (α := ℝ≥0∞) ((trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have hC_gen : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
Tactic: rw [← cylinder_univ (Iic 0), trajFun, AddContent.measure_eq, trajContent_cylinder .univ,
      measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hC_gen : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
⊢ Eq (α := ℝ≥0∞) ((trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
have hs : cylinder (α := X) (Iic 0) Set.univ ∈ measurableCylinders X
Tactic: rw [← cylinder_univ (Iic 0), trajFun, AddContent.measure_eq, trajContent_cylinder .univ,
      measure_univ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveLimit (α := X) (trajFun (X := X) κ a x₀)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x₀)
have refine : ∀ (n : ℕ),
  Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀))
    (inducedFamily (X := X)
      (fun (b : ℕ) ↦
        (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      (Iic n))
Tactic: refine isProjectiveLimit_nat_iff (isProjectiveMeasureFamily_partialTraj κ x₀) _ |>.2 fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
⊢ Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀))
    (inducedFamily (X := X)
      (fun (b : ℕ) ↦
        (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      (Iic n))
have h : ∀ (s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀) : Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((inducedFamily (X := X)
              (fun (b : ℕ) ↦
                (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x₀)
              (Iic n) :
            Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s ms
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀) : Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((inducedFamily (X := X)
              (fun (b : ℕ) ↦
                (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x₀)
              (Iic n) :
            Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
Tactic: rw [Measure.map_apply (measurable_frestrictLe n) ms, trajFun, AddContent.measure_eq, trajContent,
    projectiveFamilyContent_congr _ (frestrictLe n ⁻¹' s) rfl ms]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
n : ℕ
s : Set ((i : ↥(Iic n)) → X (↑i : ℕ))
ms : MeasurableSet s
h : MeasurableSpace.pi (X := X) = generateFrom (measurableCylinders X)
⊢ Eq (α := ℝ≥0∞)
    (((Measure.map (frestrictLe (π := X) n) (trajFun (X := X) κ a x₀) : Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((inducedFamily (X := X)
              (fun (b : ℕ) ↦
                (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x₀)
              (Iic n) :
            Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) :
          (a : Set ((i : ↥(Iic n)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : frestrictLe (π := X) n ⁻¹' s ∈ measurableCylinders X
Tactic: rw [Measure.map_apply (measurable_frestrictLe n) ms, trajFun, AddContent.measure_eq, trajContent,
    projectiveFamilyContent_congr _ (frestrictLe n ⁻¹' s) rfl ms]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ Measurable (trajFun (X := X) κ a)
have h : ∀ (s : Set ((n : ℕ) → X n)),
  MeasurableSet s →
    Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
      (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s
Tactic: apply Measure.measurable_of_measurable_coe
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ ∀ (s : Set ((n : ℕ) → X n)),
    MeasurableSet s →
      Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s
have cylinder : ∀ (t : Set ((n : ℕ) → X n)) (ht : t ∈ measurableCylinders X),
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    t sorry
Tactic: refine MeasurableSpace.induction_on_inter
    (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t))
    (s := measurableCylinders X) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (by simp) (fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl)
    (fun f disf mf hf ↦ ?union)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
cylinder :
  ∀ (t : Set ((n : ℕ) → X n)) (ht : t ∈ measurableCylinders X),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      t ⋯
⊢ ∀ (s : Set ((n : ℕ) → X n)),
    MeasurableSet s →
      Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s
have compl : ∀ (t : Set ((n : ℕ) → X n)) (mt : MeasurableSet t)
  (ht :
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      t mt),
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    tᶜ sorry
Tactic: refine MeasurableSpace.induction_on_inter
    (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t))
    (s := measurableCylinders X) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (by simp) (fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl)
    (fun f disf mf hf ↦ ?union)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
cylinder :
  ∀ (t : Set ((n : ℕ) → X n)) (ht : t ∈ measurableCylinders X),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      t ⋯
compl :
  ∀ (t : Set ((n : ℕ) → X n)) (mt : MeasurableSet t)
    (ht :
      (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
          Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
            (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
        t mt),
    (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
        Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
          (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
      tᶜ ⋯
⊢ ∀ (s : Set ((n : ℕ) → X n)),
    MeasurableSet s →
      Measurable (β := ℝ≥0∞) fun (b : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a b : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) s
have union : ∀ (f : ℕ → Set ((n : ℕ) → X n)) (disf : Pairwise (Disjoint on f)) (mf : ∀ (i : ℕ), MeasurableSet (f i))
  (hf :
    ∀ (i : ℕ),
      (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
          Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
            (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
        (f i) sorry),
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    (⋃ (i : ℕ), f i) sorry
Tactic: refine MeasurableSpace.induction_on_inter
    (C := fun t ht ↦ Measurable (fun x₀ ↦ trajFun κ a x₀ t))
    (s := measurableCylinders X) generateFrom_measurableCylinders.symm
    isPiSystem_measurableCylinders (by simp) (fun t ht ↦ ?cylinder) (fun t mt ht ↦ ?compl)
    (fun f disf mf hf ↦ ?union)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
⊢ (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    t ⋯
have cylinder : ∀ (N : ℕ) (S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))) (mS : MeasurableSet S) (t_eq : t = cylinder (α := X) (Iic N) S),
  Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t
Tactic: obtain ⟨N, S, mS, t_eq⟩ : ∃ N S, MeasurableSet S ∧ t = cylinder (Iic N) S := by
      simpa [measurableCylinders_nat] using ht
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = cylinder (α := X) (Iic N) S
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t
have cylinder : Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
  ((Measure.map (restrict₂ (π := X) sorry)
          ((partialTraj (X := X) κ a ((Iic N).sup id) :
              (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
            x₀) :
        Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) :
      (a : Set ((j : ↥(Iic N)) → X (↑j : ℕ))) → ℝ≥0∞)
    S
Tactic: simp_rw [trajFun, AddContent.measure_eq _ _ generateFrom_measurableCylinders.symm _ ht,
      trajContent, projectiveFamilyContent_congr _ t t_eq mS, inducedFamily]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
ht : t ∈ measurableCylinders X
N : ℕ
S : Set ((i : ↥(Iic N)) → X (↑i : ℕ))
mS : MeasurableSet S
t_eq : t = cylinder (α := X) (Iic N) S
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
    ((Measure.map (restrict₂ (π := X) ⋯)
            ((partialTraj (X := X) κ a ((Iic N).sup id) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
              x₀) :
          Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) :
        (a : Set ((j : ↥(Iic N)) → X (↑j : ℕ))) → ℝ≥0∞)
      S
have cylinder : Measurable (β := Measure ((k : ↥(Iic N)) → X (↑k : ℕ))) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
  Measure.map (restrict₂ (π := X) sorry)
    ((partialTraj (X := X) κ a ((Iic N).sup id) :
        (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic ((Iic N).sup id))) → X (↑i : ℕ)))
      x₀)
Tactic: refine Measure.measurable_measure.1 ?_ _ mS
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
t : Set ((n : ℕ) → X n)
mt : MeasurableSet t
ht :
  (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    t mt
⊢ (fun (t : Set ((n : ℕ) → X n)) (ht : MeasurableSet t) ↦
      Measurable (β := ℝ≥0∞) fun (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)) ↦
        (trajFun (X := X) κ a x₀ : (a : Set ((n : ℕ) → X n)) → ℝ≥0∞) t)
    tᶜ ⋯
have this : ∀ (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)), IsProbabilityMeasure (trajFun (X := X) κ a x₀)
Tactic: have := isProbabilityMeasure_trajFun κ a
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ (traj (X := X) κ a).map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
have h : ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)) (s : Set ((i : ↥(Iic b)) → X (↑i : ℕ))),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((((traj (X := X) κ a).map (frestrictLe (π := X) b) :
                  (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                x :
              Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
              Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
            (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
          s :
        ℝ≥0∞)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((((traj (X := X) κ a).map (frestrictLe (π := X) b) :
                (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
Tactic: rw [map_apply, traj_apply, frestrictLe, isProjectiveLimit_trajFun, inducedFamily_Iic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x)
have rw : Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
        (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      x :
    Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
Tactic: rw [← map_apply _ (measurable_frestrictLe b), traj_map_frestrictLe]