-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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₀))
⊢ ∀ (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)
have 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)
Tactic: rw [piLE_eq_comap_frestrictLe]