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)
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 : ℕ)
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∞)
⊢ 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₁ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
Tactic: rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_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
x : (i : ↥(Iic b)) → X (↑i : ℕ)
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∞)
h₁ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
⊢ 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₂ : MeasurableSet (α := (i : ℕ) → X i) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
Tactic: rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_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
x : (i : ↥(Iic b)) → X (↑i : ℕ)
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∞)
h₁ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
h₂ : MeasurableSet (α := (i : ℕ) → X i) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)
h₃ : Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x
⊢ 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₄ : MeasurableSet (Prod.mk x ⁻¹' s)
Tactic: rw [← traj_map_updateFinset, Measure.map_apply, Measure.map_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
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 ((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∞)
have h : ∀ (y : (i : ℕ) → X i),
  Membership.mem (γ := Set ((i : ℕ) → X i))
      ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) y ↔
    Membership.mem (γ := Set ((i : ℕ) → X i))
      (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))
      y
Tactic: congr 1 with y
-- 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 : ℕ)
y : (i : ℕ) → X i
⊢ Membership.mem (γ := Set ((i : ℕ) → X i))
      ((fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x) ⁻¹' Prod.mk x ⁻¹' s) y ↔
    Membership.mem (γ := Set ((i : ℕ) → X i))
      (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))
      y
have h : (x, updateFinset (π := X) y (Iic b) x) ∈ s ↔
  (frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x), updateFinset (π := X) y (Iic b) x) ∈ s
Tactic: simp only [Set.mem_preimage]
-- 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 : ℕ)
y : (i : ℕ) → X i
⊢ (x, updateFinset (π := X) y (Iic b) x) ∈ s ↔
    (frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x), updateFinset (π := X) y (Iic b) x) ∈ s
have h : ∀ (i : ↥(Iic b)), x i = frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x) i
Tactic: congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s
-- 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 : ℕ)
y : (i : ℕ) → X i
h : ∀ (i : ↥(Iic b)), x i = frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x) i
⊢ (x, updateFinset (π := X) y (Iic b) x) ∈ s ↔
    (frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x), updateFinset (π := X) y (Iic b) x) ∈ s
have h₁ : ∀ (i : ℕ), updateFinset (π := X) y (Iic b) x i = updateFinset (π := X) y (Iic b) x i
Tactic: congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s
-- 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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have hf : Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
  (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
  (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
    (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
Tactic: have hf : (fun x : Π n, X n ↦ (frestrictLe b x, x (b + 1))) =
      (Prod.map id (fun x ↦ x (b + 1))) ∘ (fun x ↦ (frestrictLe b x, x)) := rfl
-- 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
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
    (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have rw : (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
  Measure.map (α := (i : ℕ) → X i)
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
Tactic: rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]
-- 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
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
    (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
rw :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := (i : ℕ) → X i)
      (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
        (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((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₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have rw₁ : (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
  Measure.map (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
    (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)) x₀))
Tactic: rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]
-- 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
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
    (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
rw :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := (i : ℕ) → X i)
      (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
        (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw₁ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
      (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)) x₀))
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have rw₂ : (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
  Measure.map (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
Tactic: rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]
-- 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
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
    (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
rw :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := (i : ℕ) → X i)
      (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
        (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw₁ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
      (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)) x₀))
rw₂ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b)
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have rw₃ : (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
    (traj (X := X) κ b).map fun (x : (i : ℕ) → X i) ↦ x (b + 1)
Tactic: rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]
-- 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
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1))
    (fun (x : (n : ℕ) → X n) ↦ (frestrictLe (π := X) b x, x (b + 1)))
    (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
      (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
rw :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := (i : ℕ) → X i)
      (Function.comp (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i))
        (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1)) fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
rw₁ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
      (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)) x₀))
rw₂ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b)
rw₃ :
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      (traj (X := X) κ b).map fun (x : (i : ℕ) → X i) ↦ x (b + 1)
⊢ (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
    Measure.map (fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x (b + 1)))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
have rw₄ : (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b =
  (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ κ b
Tactic: rw [hf, ← Measure.map_map (by fun_prop) (by fun_prop), ← partialTraj_compProd_traj hab,
    ← Measure.compProd_map (by fun_prop), map_traj_succ_self]
-- 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
inst_3 : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf hf' :
  Integrable (uncurry f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) 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 x y)
    (@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 (frestrictLe (π := X) b x) x)
have hf'₁ : @Integrable _ _ _ _ Prod.instMeasurableSpace (uncurry f)
  (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)) x₀))
Tactic: rw [partialTraj_compProd_traj hab] at hf'
Cleared hypotheses: hf'