-- 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 : a ≤ b
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)))
        ⋯ :
      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 : ℕ)))
succ :
  ∀ (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 : ℕ)))
⊢ 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 : ℕ)))

Tactic:
induction b, hab using Nat.le_induction with
  | base => simp
  | succ k hak hk => rw [Nat.leRec_succ, ← partialTraj_le_def]; lia

Premises used: ProbabilityTheory.Kernel.partialTraj_le_def, Nat.leRec_succ