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 : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
rw :
  Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (((traj (X := X) κ a).map (frestrictLe (π := X) b) :
          (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        x :
      Measure ((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 : ℕ)))
⊢ 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 rw₁ : Eq (α := Measure ((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 : ℕ)))
  ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
Tactic: rw [← map_apply _ (measurable_frestrictLe b), traj_map_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)
a b : ℕ
hab : a ≤ b
⊢ (traj (X := X) κ b).map (frestrictLe (π := X) a) = deterministic (frestrictLe₂ (π := X) hab) ⋯
have rw : partialTraj (X := X) κ b a = deterministic (frestrictLe₂ (π := X) hab) sorry
Tactic: rw [traj_map_frestrictLe, partialTraj_le]
-- 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
rw : partialTraj (X := X) κ b a = deterministic (frestrictLe₂ (π := X) hab) ⋯
⊢ (traj (X := X) κ b).map (frestrictLe (π := X) a) = deterministic (frestrictLe₂ (π := X) hab) ⋯
have rw₁ : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic b)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
  (deterministic (frestrictLe₂ (π := X) hab) sorry) (deterministic (frestrictLe₂ (π := X) hab) sorry)
Tactic: rw [traj_map_frestrictLe, partialTraj_le]
-- 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 : ℕ
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a
have hf : Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
  ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) ∘
    frestrictLe (π := X) (a + 1))
Tactic: have hf : (fun x : Π n, X n ↦ x (a + 1)) =
      (fun x ↦ x ⟨a + 1, mem_Iic.2 le_rfl⟩) ∘ frestrictLe (a + 1) := 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 : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a
have rw : (traj (X := X) κ a).map
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) ∘
      frestrictLe (π := X) (a + 1)) =
  κ a
Tactic: rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_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 : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
rw :
  (traj (X := X) κ a).map
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        frestrictLe (π := X) (a + 1)) =
    κ a
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a
have rw₁ : (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
    ((traj (X := X) κ a).map (frestrictLe (π := X) (a + 1))) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) =
  κ a
Tactic: rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_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 : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
rw :
  (traj (X := X) κ a).map
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        frestrictLe (π := X) (a + 1)) =
    κ a
rw₁ :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      ((traj (X := X) κ a).map (frestrictLe (π := X) (a + 1))) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a
have rw₂ : (map (partialTraj (X := X) κ a (a + 1)) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) =
  κ a
Tactic: rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_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 : ℕ
hf :
  Eq.{u_1 + 1} (α := (x : (n : ℕ) → X n) → X (a + 1)) (fun (x : (n : ℕ) → X n) ↦ x (a + 1))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      frestrictLe (π := X) (a + 1))
rw :
  (traj (X := X) κ a).map
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        frestrictLe (π := X) (a + 1)) =
    κ a
rw₁ :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      ((traj (X := X) κ a).map (frestrictLe (π := X) (a + 1))) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
rw₂ :
  (map (partialTraj (X := X) κ a (a + 1)) fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) =
    κ a
⊢ ((traj (X := X) κ a).map fun (x : (n : ℕ) → X n) ↦ x (a + 1)) = κ a
have rw₃ : κ a = κ a
Tactic: rw [hf, map_comp_right _ (by fun_prop) (by fun_prop), traj_map_frestrictLe,
    map_partialTraj_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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
⊢ η = traj (X := X) κ a
have h : ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)),
  Eq (α := Measure ((n : ℕ) → X n))
    ((η : (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: ext x : 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq (α := Measure ((n : ℕ) → X n))
    ((η : (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))
have h : IsProjectiveLimit (α := X) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
  (inducedFamily (X := X) fun (n : ℕ) ↦
    (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
Tactic: refine ((isProjectiveLimit_trajFun _ _ _).unique ?_).symm
-- 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveLimit (α := X) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
have h : ∀ ⦃n_1 : ℕ⦄,
  n ≤ n_1 →
    Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic n_1)) → X (↑i : ℕ)))
      (Measure.map (frestrictLe (π := X) n_1) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
      (inducedFamily (X := X)
        (fun (n : ℕ) ↦
          (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
        (Iic n_1))
Tactic: rw [isProjectiveLimit_nat_iff' _ _ n]
-- 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
h :
  ∀ ⦃n_1 : ℕ⦄,
    n ≤ n_1 →
      Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic n_1)) → X (↑i : ℕ)))
        (Measure.map (frestrictLe (π := X) n_1) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
        (inducedFamily (X := X)
          (fun (n : ℕ) ↦
            (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
          (Iic n_1))
⊢ IsProjectiveLimit (α := X) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
have rw : IsProjectiveMeasureFamily (α := X)
  (inducedFamily (X := X) fun (n : ℕ) ↦
    (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
Tactic: rw [isProjectiveLimit_nat_iff' _ _ n]
-- 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
k : ℕ
hk : n ≤ k
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    (inducedFamily (X := X)
      (fun (n : ℕ) ↦
        (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
      (Iic k))
have h : Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
  (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
  ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x)
Tactic: rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]
-- 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
k : ℕ
hk : n ≤ k
h :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    (inducedFamily (X := X)
      (fun (n : ℕ) ↦
        (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
      (Iic k))
have h₁ : Eq (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
  ((η.map (frestrictLe (π := X) k) : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
  ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
Tactic: rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]
-- 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 n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
k : ℕ
hk : n ≤ k
h :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x)
h₁ :
  Eq (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((η.map (frestrictLe (π := X) k) : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    (inducedFamily (X := X)
      (fun (n : ℕ) ↦
        (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
      (Iic k))
have h₂ : Eq (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
  ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
  ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
    Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
Tactic: rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]
-- 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
⊢ traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b = traj (X := X) κ a
have refine : ∀ (n : ℕ), (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n
Tactic: refine eq_traj _ _ fun n ↦ ?_
-- 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
n : ℕ
⊢ (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n
have rw : (traj (X := X) κ b).map (frestrictLe (π := X) n) ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
Tactic: rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]
-- 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
n : ℕ
rw : (traj (X := X) κ b).map (frestrictLe (π := X) n) ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
⊢ (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n
have rw₁ : partialTraj (X := X) κ b n ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
Tactic: rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]
-- 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
n : ℕ
rw : (traj (X := X) κ b).map (frestrictLe (π := X) n) ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
rw₁ : partialTraj (X := X) κ b n ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
⊢ (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n
have rw₂ : partialTraj (X := X) κ a n = partialTraj (X := X) κ a n
Tactic: rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]
-- 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 : ℕ
⊢ traj (X := X) κ a =
    map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
have refine : ∀ (b : ℕ) (hb : b ≥ a + 1),
  map (mβ := MeasurableSpace.pi (X := X))
      (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
      (frestrictLe (π := X) b) =
    partialTraj (X := X) κ a b
Tactic: refine (eq_traj' _ (a + 1) _ fun b hb ↦ ?_).symm
-- 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β := MeasurableSpace.pi (X := X))
      (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
      (frestrictLe (π := X) b) =
    partialTraj (X := X) κ a b
have rw : 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
Tactic: rw [← 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 (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
⊢ map (mβ := MeasurableSpace.pi (X := X))
      (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
      (frestrictLe (π := X) b) =
    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 : ℕ))) (β :=
  (n : ℕ) → X n)
  (⇑(IicProdIoi (X := X) a) :
    (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
Tactic: rw [← 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 (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
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
⊢ map (mβ := MeasurableSpace.pi (X := X))
      (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
      (frestrictLe (π := X) b) =
    partialTraj (X := X) κ a b
have hg : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
Tactic: rw [← map_comp_right]