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_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a a)
have inl : IsZeroOrMarkovKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) Kernel.id
Tactic: rw [partialTraj_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b k : ℕ
hak : a ≤ k
h : IsZeroOrMarkovKernel (partialTraj (X := X) κ a k)
⊢ IsZeroOrMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
have inl : IsZeroOrMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (mβ :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic (k + 1))) ↦ X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a k)
    (_root_.IicProdIoc (X := X) k (k + 1)))
Tactic: rw [partialTraj_succ_of_le hak]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
have inl : IsZeroOrMarkovKernel (partialTraj (X := X) κ a a)
Tactic: induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
inl : IsZeroOrMarkovKernel (partialTraj (X := X) κ a a)
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
have inl₁ : ∀ (k : ℕ) (hak : a ≤ k),
  IsZeroOrMarkovKernel (partialTraj (X := X) κ a k) →
    IsZeroOrMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
Tactic: induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak => rw [partialTraj_succ_of_le hak]; infer_instance
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
have inr : IsZeroOrMarkovKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) (deterministic (frestrictLe₂ (π := X) hba) sorry)
Tactic: rw [partialTraj_le hba]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ IsMarkovKernel (partialTraj (X := X) κ a b)
have inl : ∀ (hab : a ≤ b), IsMarkovKernel (partialTraj (X := X) κ a b)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
inl : ∀ (hab : a ≤ b), IsMarkovKernel (partialTraj (X := X) κ a b)
⊢ IsMarkovKernel (partialTraj (X := X) κ a b)
have inr : ∀ (hba : b ≤ a), IsMarkovKernel (partialTraj (X := X) κ a b)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ IsMarkovKernel (partialTraj (X := X) κ a a)
have inl : IsMarkovKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) Kernel.id
Tactic: rw [partialTraj_self]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b k : ℕ
hak : a ≤ k
h : IsMarkovKernel (partialTraj (X := X) κ a k)
⊢ IsMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
have inl : IsMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (mβ :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic (k + 1))) ↦ X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a k)
    (_root_.IicProdIoc (X := X) k (k + 1)))
Tactic: rw [partialTraj_succ_of_le hak]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b k : ℕ
hak : a ≤ k
h : IsMarkovKernel (partialTraj (X := X) κ a k)
⊢ IsMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic (k + 1))) ↦ X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) ∘ₖ
        partialTraj (X := X) κ a k)
      (_root_.IicProdIoc (X := X) k (k + 1)))
have this : IsMarkovKernel (β := (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) (mβ :=
  MeasurableSpace.pi (X := fun (i : ↥(Ioc k (k + 1))) ↦ X (↑i : ℕ)))
  ((κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
Tactic: have := IsMarkovKernel.map (κ k) (piSingleton k).measurable
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsMarkovKernel (partialTraj (X := X) κ a b)
have inl : IsMarkovKernel (partialTraj (X := X) κ a a)
Tactic: induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak =>
      rw [partialTraj_succ_of_le hak]
      have := IsMarkovKernel.map (κ k) (piSingleton k).measurable
      exact IsMarkovKernel.map _ measurable_IicProdIoc
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
inl : IsMarkovKernel (partialTraj (X := X) κ a a)
⊢ IsMarkovKernel (partialTraj (X := X) κ a b)
have inl₁ : ∀ (k : ℕ) (hak : a ≤ k),
  IsMarkovKernel (partialTraj (X := X) κ a k) →
    IsMarkovKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
Tactic: induction b, hab using Nat.le_induction with
    | base => rw [partialTraj_self]; infer_instance
    | succ k hak =>
      rw [partialTraj_succ_of_le hak]
      have := IsMarkovKernel.map (κ k) (piSingleton k).measurable
      exact IsMarkovKernel.map _ measurable_IicProdIoc
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsMarkovKernel (partialTraj (X := X) κ a b)
have inr : IsMarkovKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
  MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) (deterministic (frestrictLe₂ (π := X) hba) sorry)
Tactic: rw [partialTraj_le hba]
-- 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))
a : ℕ
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (a + 1))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
have rw : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a a)
    (_root_.IicProdIoc (X := X) a (a + 1)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1)))
Tactic: rw [partialTraj_succ_of_le le_rfl, partialTraj_self, comp_id]
-- 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))
a : ℕ
rw :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
        partialTraj (X := X) κ a a)
      (_root_.IicProdIoc (X := X) a (a + 1)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (a + 1))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
have rw₁ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
      Kernel.id)
    (_root_.IicProdIoc (X := X) a (a + 1)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1)))
Tactic: rw [partialTraj_succ_of_le le_rfl, partialTraj_self, comp_id]
-- 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))
a : ℕ
rw :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
        partialTraj (X := X) κ a a)
      (_root_.IicProdIoc (X := X) a (a + 1)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
rw₁ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
        Kernel.id)
      (_root_.IicProdIoc (X := X) a (a + 1)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (a + 1))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a (a + 1)))
have rw₂ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1)))
  (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1)))
Tactic: rw [partialTraj_succ_of_le le_rfl, partialTraj_self, comp_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (partialTraj (X := X) κ b (b + 1) ∘ₖ partialTraj (X := X) κ a b)
have rw : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
  (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) b (b + 1)) ∘ₖ
    partialTraj (X := X) κ a b)
Tactic: rw [partialTraj_succ_self, ← map_comp, partialTraj_succ_of_le hab]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
rw :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) b (b + 1)) ∘ₖ
      partialTraj (X := X) κ a b)
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (partialTraj (X := X) κ b (b + 1) ∘ₖ partialTraj (X := X) κ a b)
have rw₁ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
  (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a b)
    (_root_.IicProdIoc (X := X) b (b + 1)))
Tactic: rw [partialTraj_succ_self, ← map_comp, partialTraj_succ_of_le hab]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
rw :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) b (b + 1)) ∘ₖ
      partialTraj (X := X) κ a b)
rw₁ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
        partialTraj (X := X) κ a b)
      (_root_.IicProdIoc (X := X) b (b + 1)))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (partialTraj (X := X) κ b (b + 1) ∘ₖ partialTraj (X := X) κ a b)
have rw₂ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
  (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a b)
    (_root_.IicProdIoc (X := X) b (b + 1)))
  (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
      partialTraj (X := X) κ a b)
    (_root_.IicProdIoc (X := X) b (b + 1)))
Tactic: rw [partialTraj_succ_self, ← map_comp, partialTraj_succ_of_le hab]
-- 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
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))
have succ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
  (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b)
  (partialTraj (X := X) κ a (k + 1))
Tactic: rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]
-- 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
k : ℕ
h : b ≤ k
hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k
succ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b)
    (partialTraj (X := X) κ a (k + 1))
⊢ 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))
have succ₁ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
  (partialTraj (X := X) κ k (k + 1) ∘ₖ (partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b))
  (partialTraj (X := X) κ a (k + 1))
Tactic: rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]
-- 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
k : ℕ
h : b ≤ k
hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k
succ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b)
    (partialTraj (X := X) κ a (k + 1))
succ₁ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ (partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b))
    (partialTraj (X := X) κ a (k + 1))
⊢ 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))
have succ₂ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
  (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ a k) (partialTraj (X := X) κ a (k + 1))
Tactic: rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]
-- 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
k : ℕ
h : b ≤ k
hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k
succ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b)
    (partialTraj (X := X) κ a (k + 1))
succ₁ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ (partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b))
    (partialTraj (X := X) κ a (k + 1))
succ₂ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ a k) (partialTraj (X := X) κ a (k + 1))
⊢ 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))
have succ₃ : Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (k + 1))
  (partialTraj (X := X) κ a (k + 1))
Tactic: rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]