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 : ℕ
hb : b ≥ a + 1
| map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
    (frestrictLe (π := X) b ∘
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
have enter : frestrictLe (π := X) b ∘
  (⇑(IicProdIoi (X := X) a) :
    (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
Tactic: enter [2]
-- 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 : ℕ
hb : b ≥ a + 1
| frestrictLe (π := X) b ∘
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
have change : Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
  (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry))
Tactic: change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).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)
a b : ℕ
hb : b ≥ a + 1
| map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
    (frestrictLe (π := X) b ∘
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
have enter : Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
  (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry))
Tactic: enter [2]; change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).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)
a b : ℕ
hb : b ≥ a + 1
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (frestrictLe (π := X) b ∘
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)) =
    partialTraj (X := X) κ a b
have conv_lhs : map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
    (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      (_root_.IicProdIoc (X := X) a b)
      (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
        x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry))) =
  partialTraj (X := X) κ a b
Tactic: conv_lhs => enter [2]; change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).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)
a b : ℕ
hb : b ≥ a + 1
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have rw : map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (map Kernel.id id ×ₖ
      (traj (X := X) κ a).map
        ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry)) ∘
          (Set.Ioi a).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b) =
  partialTraj (X := X) κ a b
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have hg : Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
  fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
  x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry)
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id
hg₁ :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have rw₂ : MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id
hg₁ :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₂ : MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have hf₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
  ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
  (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry))
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id
hg₁ :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₂ : MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))
hf₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
have hg₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) a b)
Tactic: rw [map_comp_right, ← map_prod_map, ← map_comp_right]
-- 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 : ℕ
hb : b ≥ a + 1
| map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (map Kernel.id id ×ₖ
      (traj (X := X) κ a).map
        ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
          (Set.Ioi a).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b)
have enter : (fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) sorry)) ∘
  (Set.Ioi a).restrict (π := X)
Tactic: enter [1, 2, 2]
-- 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 : ℕ
hb : b ≥ a + 1
| (fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
    (Set.Ioi a).restrict (π := X)
have change : (Ioc a b).restrict (π := X)
Tactic: change (Ioc a b).restrict
-- 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 : ℕ
hb : b ≥ a + 1
| map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (map Kernel.id id ×ₖ
      (traj (X := X) κ a).map
        ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
          (Set.Ioi a).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b)
have enter : (Ioc a b).restrict (π := X)
Tactic: enter [1, 2, 2]; change (Ioc a b).restrict
-- 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 : ℕ
hb : b ≥ a + 1
⊢ map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
have conv_lhs : map (mβ := Prod.instMeasurableSpace) (map Kernel.id id ×ₖ (traj (X := X) κ a).map ((Ioc a b).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b) =
  partialTraj (X := X) κ a b
Tactic: conv_lhs => enter [1, 2, 2]; change (Ioc a b).restrict
-- 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 : ℕ
hb : b ≥ a + 1
⊢ map (mβ := Prod.instMeasurableSpace) (map Kernel.id id ×ₖ (traj (X := X) κ a).map ((Ioc a b).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
have hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
Tactic: rw [← restrict₂_comp_restrict Ioc_subset_Iic_self, ← frestrictLe, map_comp_right,
        traj_map_frestrictLe, map_id, ← partialTraj_eq_prod]
-- 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 : ℕ
hb : b ≥ a + 1
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
⊢ map (mβ := Prod.instMeasurableSpace) (map Kernel.id id ×ₖ (traj (X := X) κ a).map ((Ioc a b).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
have hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
Tactic: rw [← restrict₂_comp_restrict Ioc_subset_Iic_self, ← frestrictLe, map_comp_right,
        traj_map_frestrictLe, map_id, ← partialTraj_eq_prod]
-- 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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
have nth_rw : Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
  (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
  ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
        (⇑(IicProdIoi (X := X) n) :
          (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
      (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
    x)
Tactic: nth_rw 2 [traj_eq_prod]
-- 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)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
⊢ Eq (α := ((i : ℕ) → X i) → (i : ℕ) → X i) (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
    ((⇑(IicProdIoi (X := X) n) :
        (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
      Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
have h : ∀ (x_1 : (i : ℕ) → X i) (x_2 : ℕ),
  updateFinset (π := X) x_1 (Iic n) x x_2 =
    ((⇑(IicProdIoi (X := X) n) :
          (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) ∘
        Prod.mk x ∘ (Set.Ioi n).restrict (π := X))
      x_1 x_2
Tactic: ext