-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst_2 : NormedAddCommGroup E
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
hf' :
  @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
simp_rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        uncurry f (x, y))
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      uncurry f (frestrictLe (π := X) b x, x))
simp_rw₁ :
  Eq.{u_2 + 1} (α := E)
    (∫ (x : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)),
      uncurry f
        x ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ ⊗ₘ
        traj (X := X) κ b)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      uncurry f (frestrictLe (π := X) b x, x))
simp_rw₂ :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ Prod.instMeasurableSpace
      (Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
      fun (x : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) ↦ uncurry f x)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      uncurry f (frestrictLe (π := X) b x, x))
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
      fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
      @integral _ _ _ _ (MeasurableSpace.pi (X := X))
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x) fun (y : (n : ℕ) → X n) ↦
        f x y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) fun (x : (n : ℕ) → X n) ↦
      f (frestrictLe (π := X) b x) x)

Tactic:
simp_rw [← uncurry_apply_pair f, ← Measure.integral_compProd hf,
    partialTraj_compProd_traj hab, integral_map (by fun_prop) hf'.1]

Premises used: MeasureTheory.integral_map, ProbabilityTheory.Kernel.partialTraj_compProd_traj, MeasureTheory.Measure.integral_compProd, And.left, Function.uncurry_apply_pair