-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
inl₅ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (β :=
    ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) ⋯) id)
inl₆ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₇ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) n (n + 1))
inl₈ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic (n + 1))) → X (↑i : ℕ)) (β := (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)
inl₉ :
  Measurable.{u_1, u_1} (α := X (n + 1)) (β := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))

Tactic:
rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]

Premises used: ProbabilityTheory.Kernel.partialTraj_succ_of_le, ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.map_comp_right, MeasureTheory.Measure.map_piSingleton, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.prod_const_comp, MeasureTheory.Measure.pi_prod_map_IocProdIoc, ProbabilityTheory.Kernel.map_const, ProbabilityTheory.Kernel.id_comp, ProbabilityTheory.Kernel.map_prod_map, ProbabilityTheory.Kernel.const_apply, ProbabilityTheory.Kernel.map_id