-- 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
inst_4 : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_cf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X))
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
mcf :
  StronglyMeasurable
    (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
x : (n : ℕ) → X n
h1 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((n : ℕ) → X n)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x
h2 :
  condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
      (condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f)
      x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y
h :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (y : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f y)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
      fun (x_1 : (n : ℕ) → X n) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) (frestrictLe (π := X) c x_1)))
h₁ :
  AEMeasurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic c)) → X (↑i : ℕ)) (_m := MeasurableSpace.pi (X := X))
    (frestrictLe (π := X) c)
    ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x))
h₂ :
  AEStronglyMeasurable.{u_1, u_2} (β := E) (m₀ := MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
    (fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) y))
    (Measure.map (frestrictLe (π := X) c)
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) (frestrictLe (π := X) b x)))
h₃ : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic c)) → X (↑i : ℕ)) (frestrictLe (π := X) c)
⊢ condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) b) (m₀ := MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f x =
    @integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic c)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x))
      fun (y : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦
      condExp ((↑(piLE (X := X)) : ℕ → MeasurableSpace ((i : ℕ) → X i)) c) (m₀ := MeasurableSpace.pi (X := X))
        ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) f
        (updateFinset (π := X) x (Iic c) y)

Tactic:
rw [← h1, h2, ← traj_map_frestrictLe, Kernel.map_apply, integral_map]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.integral_map, ProbabilityTheory.Kernel.traj_map_frestrictLe