awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
hbc : b ≤ c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have base : partialTraj (X := X) κ b b ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a b
Tactic: induction c, hbc using Nat.le_induction with
  | base => simp
  | succ k h hk => rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
hbc : b ≤ c
base : partialTraj (X := X) κ b b ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a b
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
have succ : ∀ (k : ℕ) (h : b ≤ k) (hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k),
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ b (k + 1) ∘ₖ partialTraj (X := X) κ a b) (partialTraj (X := X) κ a (k + 1))
Tactic: induction c, hbc using Nat.le_induction with
  | base => simp
  | succ k h hk => rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]
Cleared hypotheses: hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
⊢ deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) = Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))
have h : ∀ (x : X) (s : Set (X × Z)) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst sorry ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext x s ms
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (b : X × Y),
    (((deterministic Prod.fst sorry ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
      s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
  (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
h :
  ∫⁻ (b : X × Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : ∫⁻ (b : Y),
    (((deterministic Prod.fst sorry ×ₖ η : (a : X × Y) → Measure (X × Z)) (x, b) : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s ∂(κ : (a : X) → Measure Y) x =
  (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
h :
  ∫⁻ (b : X × Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) (x, b) : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₂ : ∫⁻ (b : Y),
    (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
      (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
  (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
    s
Tactic: simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
h :
  ∫⁻ (b : X × Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) (x, b) : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₃ : ∫⁻ (b : Y),
    (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
      (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
  (((η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure Z) x : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
Tactic: simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
h :
  ∫⁻ (b : X × Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) (x, b) : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₃ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    (((η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure Z) x : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₄ : ∫⁻ (b : Y),
    (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
      (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
  ∫⁻ (b : X × Y),
    (((η : (a : X × Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞)
      (Prod.mk x ⁻¹' s) ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x
Tactic: simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inl : ∀ (hba : b ≤ a),
  partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry)) (_root_.IicProdIoc (X := X) a b)
Tactic: obtain hba | hab := le_total b a
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
inl :
  ∀ (hba : b ≤ a),
    partialTraj (X := X) κ a b =
      map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inr : ∀ (hab : a ≤ b),
  partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry)) (_root_.IicProdIoc (X := X) a b)
Tactic: obtain hba | hab := le_total b a
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inl : Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
Tactic: rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map,
      fst_prod, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
inl :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inl₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst
Tactic: rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map,
      fst_prod, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
inl :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inl₂ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hba)
Tactic: rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map,
      fst_prod, id_map]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
⊢ partialTraj (X := X) κ a a =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a a)
have inr : ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)),
  Eq (α := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
            (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) sorry)) (_root_.IicProdIoc (X := X) a a) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
Tactic: ext1 x
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq (α := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
            (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a a) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
have inr : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) a a)
Tactic: rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
inr :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a a)
⊢ Eq (α := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
            (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a a) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
have inr₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a)) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
Tactic: rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk :
  partialTraj (X := X) κ a k =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a k).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a k)
⊢ Eq.{u_1 + 1} (α :=
    (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) →
      (i : ↥(Iic (k + 1))) → X (↑i : ℕ))
    (_root_.IicProdIoc (X := X) k (k + 1) ∘ Prod.map (_root_.IicProdIoc (X := X) a k) id)
    (Function.comp (β :=
      ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
      ((⇑(MeasurableEquiv.IicProdIoc (X := X) ⋯) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))) →
            (i : ↥(Iic k.succ)) → X (↑i : ℕ)) ∘
        Prod.map id (IocProdIoc (X := X) a k (k + 1)))
      (⇑prodAssoc :
        (a_1 :
            (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
          ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))))
have h₁ : ∀ (x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
  (i : ↥(Iic (k + 1))),
  (_root_.IicProdIoc (X := X) k (k + 1) ∘ Prod.map (_root_.IicProdIoc (X := X) a k) id) x i =
    Function.comp (β :=
      ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
      ((⇑(MeasurableEquiv.IicProdIoc (X := X) sorry) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))) →
            (i : ↥(Iic k.succ)) → X (↑i : ℕ)) ∘
        Prod.map id (IocProdIoc (X := X) a k (k + 1)))
      (⇑prodAssoc :
        (a_1 :
            (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
          ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
      x i
Tactic: ext x i