-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
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) ⋯
      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)))
          ⋯ :
      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 : ℕ)))
inr₁ inr₂ :
  Eq.{u_1 + 1} (α := 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 : 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)) → 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 : ℕ)))
⊢ 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

Tactic:
rw [partialTraj, dif_neg (not_le.2 hab)]

Premises used: not_le, Iff.mpr, dif_neg, ProbabilityTheory.Kernel.partialTraj