awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ ∀ᵐ (y :
    (i : ↥(Iic b)) →
      X
        (↑i :
          ℕ)) ∂Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀),
    @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
have h : Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Measure.map (frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
Tactic: convert! i_f.1
-- 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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
have h : Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Measure.map (frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
      (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    x₀)
Tactic: rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]
-- 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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
i_f :
  (∀ᵐ (y :
      (i : ↥(Iic b)) →
        X
          (↑i :
            ℕ)) ∂((partialTraj (X := X) κ a b :
            (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
          x₀ :
        Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
      @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
        ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)) ∧
    @Integrable ℝ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (fun (y : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦
        @integral _ _ _ _ (MeasurableSpace.pi (X := X))
          ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) y)
          fun (z : (n : ℕ) → X n) ↦ ‖f z‖)
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
h :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
        (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      x₀)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) b)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)
have h₁ : Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (Measure.map (frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  (Measure.map (frestrictLe (π := X) b)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ℕ) → X i)) x₀))
Tactic: rw [← traj_map_frestrictLe, Kernel.map_apply _ (measurable_frestrictLe _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ ∀ᵐ (x :
    (i : ↥(Iic b)) →
      X
        (↑i :
          ℕ)) ∂((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Iic b)) → X (↑i : ℕ))),
    AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
      ((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
have hf₁ : AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
  ((traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: rw [← traj_comp_partialTraj hab] at hf
Cleared hypotheses: hf
-- 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
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Eq.{u_2 + 1} (α := E)
    (@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 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) ↦
      f (updateFinset (π := X) x (Iic a) x₀))
have hφ : AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
  (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: nth_rw 1 [← traj_map_updateFinset, integral_map]
-- 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
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
hφ :
  AEMeasurable (β := (n : ℕ) → X n) (_m := MeasurableSpace.pi (X := X))
    (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Eq.{u_2 + 1} (α := E)
    (@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 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) ↦
      f (updateFinset (π := X) x (Iic a) x₀))
have hfm : AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
Tactic: nth_rw 1 [← traj_map_updateFinset, integral_map]
-- 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
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
have h : Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEStronglyMeasurable._auto_1)
  (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: convert! mf
-- 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
a : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
mf :
  AEStronglyMeasurable (m₀ := MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Eq.{u_1 + 1} (α := autoParam (Measure ((n : ℕ) → X n)) AEStronglyMeasurable._auto_1)
    (Measure.map (fun (x : (i : ℕ) → X i) ↦ updateFinset (π := X) x (Iic a) x₀)
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have h : Eq (α := autoParam (Measure ((n : ℕ) → X n)) AEStronglyMeasurable._auto_1)
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))
  ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀ : Measure ((n : ℕ) → X n))
Tactic: rw [traj_map_updateFinset]
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b =
    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)) u)
have h : ∀ (s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
            traj (X := X) κ b :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((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)) u) :
            Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext s ms
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
            traj (X := X) κ b :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((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)) u) :
            Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h : ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
    (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
        (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
      (Prod.mk a ⁻¹'
        s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u =
  ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
    (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 : Measure ((n : ℕ) → X n)) :
        (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
      ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
        s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u
Tactic: rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
h :
  ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk a ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 :
            Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u
⊢ Eq (α := ℝ≥0∞)
    (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
            traj (X := X) κ b :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((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)) u) :
            Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₁ : MeasurableSet (α := (n : ℕ) → X n) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
Tactic: rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
h :
  ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk a ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 :
            Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u
h₁ : MeasurableSet (α := (n : ℕ) → X n) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
h₂ : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    (((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
            traj (X := X) κ b :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    (((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)) u) :
            Measure (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))) :
          (a : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have h₃ : Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) fun (x : (i : ℕ) → X i) ↦
  (frestrictLe (π := X) b x, x)
Tactic: rw [Measure.map_apply, Measure.compProd_apply, ← traj_comp_partialTraj hab, comp_apply']
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) a : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk a ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        u =
    ∫⁻ (b_1 : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) b_1 :
            Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹'
          s) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u
have h : ∀ (x : (i : ↥(Iic b)) → X (↑i : ℕ)),
  Eq (α := ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) :
      ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s) :
      ℝ≥0∞)
Tactic: congr 1 with x
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
x : (i : ↥(Iic b)) → X (↑i : ℕ)
⊢ Eq (α := ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) :
      ℝ≥0∞)
    ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
          (a : Set ((n : ℕ) → X n)) → ℝ≥0∞)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s) :
      ℝ≥0∞)
have h : Eq (α := ℝ≥0∞)
  ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
        (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
      ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) :
    ℝ≥0∞)
  ((((traj (X := X) κ b : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x : Measure ((n : ℕ) → X n)) :
        (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
      (Set.preimage (β := (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x)
        ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)) :
    ℝ≥0∞)
Tactic: rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_apply]