-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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 : ℕ
hab : a ≤ b
inr :
  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)
inr₁ :
  ∀ (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 (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
      (partialTraj (X := X) κ a (k + 1))
      (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ map (partialTraj (X := X) κ a (k + 1)) (restrict₂ (π := X) ⋯))
        (_root_.IicProdIoc (X := X) a (k + 1)))
⊢ 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)

Tactic:
induction b, hab using Nat.le_induction with
  | base =>
    ext1 x
    rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]
    all_goals fun_prop
  | succ k h hk =>
    have : (IicProdIoc (X := X) k (k + 1)) ∘ (Prod.map (IicProdIoc a k) id) =
        (IicProdIoc (h.trans k.le_succ) ∘ (Prod.map id (IocProdIoc a k (k + 1)))) ∘
        prodAssoc := by
      ext x i
      simp only [IicProdIoc_def, MeasurableEquiv.IicProdIoc, MeasurableEquiv.coe_mk,
        Equiv.coe_fn_mk, Function.comp_apply, Prod.map_fst, Prod.map_snd, id_eq,
        Nat.succ_eq_add_one, IocProdIoc]
      split_ifs <;> try rfl
      lia
    nth_rw 1 [← partialTraj_comp_partialTraj h k.le_succ, hk, partialTraj_succ_self, comp_map,
      comap_map_comm, comap_prod, id_comap, ← id_map, map_prod_eq, ← map_comp_right, this,
      map_comp_right, id_prod_eq, prodAssoc_prod, map_comp_right, ← map_prod_map, map_id,
      ← map_comp, map_apply_eq_iff_map_symm_apply_eq, fst_prod_comp_id_prod, ← map_comp_right,
      ← coe_IicProdIoc (h.trans k.le_succ), symm_comp_self, map_id,
      deterministic_congr IicProdIoc_comp_restrict₂.symm, ← deterministic_comp_deterministic,
      comp_deterministic_eq_comap, ← comap_prod, ← map_comp, ← comp_map, ← hk,
      ← partialTraj_comp_partialTraj h k.le_succ, partialTraj_succ_self, map_comp, map_comp,
      ← map_comp_right, ← id_map, map_prod_eq, ← map_comp_right]
    · rfl
    all_goals fun_prop

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.Measure.fst_prod, ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.map_prod_eq, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.deterministic_comp_deterministic, ProbabilityTheory.Kernel.id_map, ProbabilityTheory.Kernel.prodAssoc_prod, ProbabilityTheory.Kernel.comap_prod, ProbabilityTheory.Kernel.partialTraj_succ_self, ProbabilityTheory.Kernel.map_comp, _private.0.ProbabilityTheory.Kernel.fst_prod_comp_id_prod, ProbabilityTheory.Kernel.comp_map, ProbabilityTheory.Kernel.partialTraj_self, IicProdIoc_self, MeasurableEquiv.symm_comp_self, ProbabilityTheory.Kernel.id_comap, ProbabilityTheory.Kernel.map_prod_map, IicProdIoc_comp_restrict₂, ProbabilityTheory.Kernel.comp_deterministic_eq_comap, Eq.symm, ProbabilityTheory.Kernel.id_prod_eq, ProbabilityTheory.Kernel.comap_map_comm, ProbabilityTheory.Kernel.map_apply_eq_iff_map_symm_apply_eq, ProbabilityTheory.Kernel.map_id, ProbabilityTheory.Kernel.deterministic_congr, MeasureTheory.Measure.fst