-- 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
⊢ 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)))

Tactic:
exact (mcf.comp_measurable measurable_updateFinset).aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, measurable_updateFinset, MeasureTheory.StronglyMeasurable.comp_measurable