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)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a : ℕ
⊢ partialTraj (X := X) κ a a = Kernel.id
have rw : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
  (deterministic (frestrictLe₂ (π := X) sorry) sorry) Kernel.id
Tactic: rw [partialTraj_le le_rfl]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic 0)) → X (↑i : ℕ))) (partialTraj (X := X) κ a 0)
    (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)
have rw : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic 0)) → X (↑i : ℕ)))
  (deterministic (frestrictLe₂ (π := X) sorry) sorry) (deterministic (frestrictLe₂ (π := X) sorry) sorry)
Tactic: rw [partialTraj_le zero_le]
-- 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
⊢ partialTraj (X := X) κ a b =
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab
have inl : ∀ (hab : a ≤ a),
  partialTraj (X := X) κ a a =
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab
Tactic: obtain rfl | hab := eq_or_lt_of_le hab
Cleared hypotheses: b, 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
inl :
  ∀ (hab : a ≤ a),
    partialTraj (X := X) κ a a =
      Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k)
            (κ_k :
              (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
                k x) ↦
          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 : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        hab
⊢ partialTraj (X := X) κ a b =
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab
have inr : ∀ (hab_1 : a < b),
  partialTraj (X := X) κ a b =
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab
Tactic: obtain rfl | hab := eq_or_lt_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_1 : a ≤ b
hab : a < b
⊢ partialTraj (X := X) κ a b =
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab_1
have inr : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (if h : b ≤ a then deterministic (frestrictLe₂ (π := X) h) sorry
    else
      Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        sorry :
    Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k)
          (κ_k :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      hab_1 :
    Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
Tactic: rw [partialTraj, dif_neg (not_le.2 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
⊢ 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)))
have rw : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
  (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      sorry :
    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)) :
    Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
Tactic: rw [partialTraj, dif_neg (by lia)]
-- 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))
k : ℕ
hak : a ≤ k
hk :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((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)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))
    (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)) × ((i : ↥(Ioc (k + 1) (k + 1 + 1))) → X (↑i : ℕ))) (mβ :=
        Prod.instMeasurableSpace)
        (Kernel.id ×ₖ
            map (κ (k + 1))
              (⇑(piSingleton (X := X) (k + 1)) : (a : X (k + 1 + 1)) → (i : ↥(Ioc (k + 1) (k + 1 + 1))) → X (↑i : ℕ)) ∘ₖ
          partialTraj (X := X) κ a (k + 1))
        (_root_.IicProdIoc (X := X) (k + 1) (k + 1 + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))
have succ : a ≤ k + 1
Tactic: rw [Nat.leRec_succ, ← partialTraj_le_def]
-- 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.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
    (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        ⋯ :
      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)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
have base : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
  (Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → 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 : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      sorry :
    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)) :
    Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
Tactic: induction b, hab using Nat.le_induction with
  | base => simp
  | succ k hak hk => rw [Nat.leRec_succ, ← partialTraj_le_def]; lia
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))
a b : ℕ
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)
have inl : ∀ (hab : a ≤ b), IsSFiniteKernel (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))
a b : ℕ
inl : ∀ (hab : a ≤ b), IsSFiniteKernel (partialTraj (X := X) κ a b)
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)
have inr : ∀ (hba : b ≤ a), IsSFiniteKernel (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))
a b : ℕ
⊢ IsSFiniteKernel (partialTraj (X := X) κ a a)
have inl : IsSFiniteKernel.{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))
a b k : ℕ
hak : a ≤ k
h : IsSFiniteKernel (partialTraj (X := X) κ a k)
⊢ IsSFiniteKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
have inl : IsSFiniteKernel (β := (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))
a b : ℕ
hab : a ≤ b
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)
have inl : IsSFiniteKernel (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))
a b : ℕ
hab : a ≤ b
inl : IsSFiniteKernel (partialTraj (X := X) κ a a)
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)
have inl₁ : ∀ (k : ℕ) (hak : a ≤ k),
  IsSFiniteKernel (partialTraj (X := X) κ a k) →
    IsSFiniteKernel (β := (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))
a b : ℕ
hba : b ≤ a
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)
have inr : IsSFiniteKernel.{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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
⊢ IsFiniteKernel (partialTraj (X := X) κ a b)
have inl : ∀ (hab : a ≤ b), IsFiniteKernel (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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
inl : ∀ (hab : a ≤ b), IsFiniteKernel (partialTraj (X := X) κ a b)
⊢ IsFiniteKernel (partialTraj (X := X) κ a b)
have inr : ∀ (hba : b ≤ a), IsFiniteKernel (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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
⊢ IsFiniteKernel (partialTraj (X := X) κ a a)
have inl : IsFiniteKernel.{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 : ℕ), IsFiniteKernel (κ n)
a b k : ℕ
hak : a ≤ k
h : IsFiniteKernel (partialTraj (X := X) κ a k)
⊢ IsFiniteKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))
have inl : IsFiniteKernel (β := (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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ IsFiniteKernel (partialTraj (X := X) κ a b)
have inl : IsFiniteKernel (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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
inl : IsFiniteKernel (partialTraj (X := X) κ a a)
⊢ IsFiniteKernel (partialTraj (X := X) κ a b)
have inl₁ : ∀ (k : ℕ) (hak : a ≤ k),
  IsFiniteKernel (partialTraj (X := X) κ a k) →
    IsFiniteKernel (β := (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 : ℕ), IsFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ IsFiniteKernel (partialTraj (X := X) κ a b)
have inr : IsFiniteKernel.{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 : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
have inl : ∀ (hab : a ≤ b), IsZeroOrMarkovKernel (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 : ℕ), IsZeroOrMarkovKernel (κ n)
a b : ℕ
inl : ∀ (hab : a ≤ b), IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
⊢ IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
have inr : ∀ (hba : b ≤ a), IsZeroOrMarkovKernel (partialTraj (X := X) κ a b)
Tactic: obtain hab | hba := le_total a b