awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
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 :
  (x, updateFinset (π := X) y (Iic b) x) ∈ s ↔
    (frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x), updateFinset (π := X) y (Iic b) x) ∈ s
⊢ 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:
simp only [Set.mem_preimage]

Premises used: Set.mem_preimage
-- 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)
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
h₁ : ∀ (i : ℕ), updateFinset (π := X) y (Iic b) x i = 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

Tactic:
congrm (fun i ↦ ?_, fun i ↦ ?_) ∈ s

Premises used: Prod.mk
-- 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)
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
i : ↥(Iic b)
⊢ x i = frestrictLe (π := X) b (updateFinset (π := X) y (Iic b) x) i

Tactic:
simp [updateFinset]

Premises used: Function.updateFinset
-- 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)
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
i : ℕ
⊢ updateFinset (π := X) y (Iic b) x i = updateFinset (π := X) y (Iic b) x i

Tactic:
simp [updateFinset]

Premises used: Function.updateFinset
-- 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)
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 : ℕ)
⊢ Measurable (β := (i : ℕ) → X i) fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic b) x

Tactic:
fun_prop
-- 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)
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 : ℕ)
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) b x, x)

Tactic:
fun_prop
-- 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)
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 : ℕ)
⊢ MeasurableSet (α := (i : ℕ) → X i) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- 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)
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 : ℕ)
⊢ Measurable (α := (i : ℕ) → X i) (Prod.mk x)

Tactic:
fun_prop
-- 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)
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 : ℕ)
⊢ MeasurableSet (Prod.mk x ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) b x, x)

Tactic:
fun_prop
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet (α := (n : ℕ) → X n) ((fun (x : (i : ℕ) → X i) ↦ (frestrictLe (π := X) b x, x)) ⁻¹' s)

Tactic:
exact ms.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
    fun (x : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) ↦ x

Tactic:
fun_prop
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact ms.preimage (by fun_prop)

Premises used: MeasurableSet.preimage
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
    fun (x : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) ↦ x

Tactic:
fun_prop
-- 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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set (((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) b x, x)

Tactic:
fun_prop
-- 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)
a b : ℕ
hab : a ≤ b
x₀ : (n : ↥(Iic a)) → X (↑n : ℕ)
⊢ 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
-- 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)
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))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) (β :=
    ((i : ↥(Iic b)) → X (↑i : ℕ)) × X (b + 1)) (Prod.map id fun (x : (i : ℕ) → X i) ↦ x (b + 1))

Tactic:
fun_prop
-- 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)
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))
⊢ Measurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ℕ) → X i)) fun (x : (i : ℕ) → X i) ↦
    (frestrictLe (π := X) b x, x)

Tactic:
fun_prop
-- 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)
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))
⊢ Measurable (β := X (b + 1)) fun (x : (i : ℕ) → X i) ↦ x (b + 1)

Tactic:
fun_prop
-- 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)
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)
rw₄ 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
⊢ (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₀)

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]

Premises used: ProbabilityTheory.Kernel.partialTraj_compProd_traj, MeasureTheory.Measure.compProd_map, ProbabilityTheory.Kernel.map_traj_succ_self, MeasureTheory.Measure.map_map
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
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)
⊢ 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)

Tactic:
have hf' := hf
-- 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
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)
⊢ @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'

Premises used: ProbabilityTheory.Kernel.partialTraj_compProd_traj
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
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)
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₀))
⊢ AEMeasurable (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) (_m := MeasurableSpace.pi (X := X))
    (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:
fun_prop
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
apply :
  Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ 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 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 x)

Tactic:
apply integral_traj_partialTraj' hab

Premises used: ProbabilityTheory.Kernel.integral_traj_partialTraj'
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  @Integrable _ _ _ _ (MeasurableSpace.pi (X := X)) f
    ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x₀)
⊢ Integrable f
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b).snd

Tactic:
rw [← traj_comp_partialTraj hab, comp_apply, ← Measure.snd_compProd] at hf

Premises used: MeasureTheory.Measure.snd_compProd, ProbabilityTheory.Kernel.traj_comp_partialTraj, ProbabilityTheory.Kernel.comp_apply
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  Integrable f
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b).snd
⊢ Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)

Tactic:
hf.comp_measurable measurable_snd

Premises used: MeasureTheory.Integrable.comp_measurable, measurable_snd
-- 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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((n : ℕ) → X n) → E
hf :
  Integrable f
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
        traj (X := X) κ b).snd
⊢ Integrable.{u_2, u_1} (ε := E) (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ ⊗ₘ
      traj (X := X) κ b)

Tactic:
exact hf.comp_measurable measurable_snd

Premises used: MeasureTheory.Integrable.comp_measurable, measurable_snd
-- 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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X (↑i : ℕ)
f : ((i : ↥(Iic b)) → X (↑i : ℕ)) → ((n : ℕ) → X n) → E
hf :
  Integrable (uncurry f)
    ((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 : ℕ))
hA : MeasurableSet A
rw :
  Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := X))
      ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u) fun (x : (n : ℕ) → X n) ↦
      A.indicator (fun (x_1 : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x_1 x) (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)) u)
        (frestrictLe (π := X) b ⁻¹' A))
      fun (y : (n : ℕ) → X n) ↦ f (frestrictLe (π := X) b y) y)
rw₁ :
  Integrable.{u_2, u_1} (ε := E)
    (uncurry fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) (y : (n : ℕ) → X n) ↦
      A.indicator (fun (x : (i : ↥(Iic b)) → X (↑i : ℕ)) ↦ f x y) x)
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u ⊗ₘ
      traj (X := X) κ b)
⊢ Eq.{u_2 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (i : ↥(Iic b)) ↦ X (↑i : ℕ)))
      (Measure.restrict
        ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) u) A)
      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))
      (Measure.restrict ((traj (X := X) κ a : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) u)
        (frestrictLe (π := X) b ⁻¹' A))
      fun (y : (n : ℕ) → X n) ↦ f (frestrictLe (π := X) b y) y)

Tactic:
rw [← integral_integral_indicator _ _ _ hA, integral_traj_partialTraj' hab]

Premises used: ProbabilityTheory.Kernel.integral_traj_partialTraj', ProbabilityTheory.Kernel.integral_integral_indicator