-- 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 : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
i_f :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
i_f' :
  @Integrable.{u_2, u_1} E _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
    (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 y)
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
refine_1 :
  ∀ (s : Set ((i : ℕ) → X i)),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞)
          ((((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ :
                  Measure ((n : ℕ) → X n)) :
                (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
              s :
            ℝ≥0∞)
          (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E)
          (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
            (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) s)
            fun (x : (i : ℕ) → X i) ↦
            ((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 y) ∘
                frestrictLe (π := X) b)
              x)
          (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
            (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀) s)
            fun (x : (i : ℕ) → X i) ↦ f x)
refine_2 :
  AEStronglyMeasurable.{u_1, u_2} (α := (i : ℕ) → X i) (β := E) (m₀ := MeasurableSpace.pi (X := 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 y) ∘
      frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ 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 =ᶠ[ae (F := Measure ((n : ℕ) → X n))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))]
    fun (x : (n : ℕ) → X n) ↦
    @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) ↦ f y

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq (piLE.le _) i_f
    (fun s _ _ ↦ i_f'.comp_aemeasurable (measurable_frestrictLe b).aemeasurable |>.integrableOn)
    ?_ ?_ |>.symm

Premises used: MeasureTheory.Integrable.comp_aemeasurable, Measurable.aemeasurable, MeasureTheory.Filtration.piLE, MeasureTheory.Filtration.le, Preorder.measurable_frestrictLe, MeasureTheory.Integrable.integrableOn, MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq, Filter.EventuallyEq.symm