awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk :
  partialTraj (X := X) κ a k =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a k).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a k)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
⊢ Eq.{u_1 + 1} (α := X (↑i : ℕ))
    (if h : (↑i : ℕ) ≤ k then
      if h_1 : (↑i : ℕ) ≤ a then x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)
      else x.1.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)
    else x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯))
    (if h : (↑i : ℕ) ≤ a then
      ((prodAssoc :
              (a_1 :
                  (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                    ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
            x).1
        (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)
    else
      if h_1 : (↑i : ℕ) ≤ k then
        ((prodAssoc :
                  (a_1 :
                      (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                        ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                    ((i : ↥(Iic a)) → X (↑i : ℕ)) ×
                      ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
                x).2.1
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)
      else
        ((prodAssoc :
                  (a_1 :
                      (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                        ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
                    ((i : ↥(Iic a)) → X (↑i : ℕ)) ×
                      ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
                x).2.2
          (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯))
have pos : ∀ (h : (↑i : ℕ) ≤ k) (h_1 : (↑i : ℕ) ≤ a),
  x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) sorry) =
    ((prodAssoc :
            (a_1 :
                (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) ×
                  ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
              ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
          x).1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) sorry)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b k : ℕ
h : a ≤ k
hk :
  partialTraj (X := X) κ a k =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a k).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a k)
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (k + 1))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ map (partialTraj (X := X) κ a (k + 1)) (restrict₂ (π := X) ⋯))
      (_root_.IicProdIoc (X := X) a (k + 1)))
have this : Eq.{u_1 + 1} (α :=
  (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) →
    (i : ↥(Iic (k + 1))) → X (↑i : ℕ))
  (_root_.IicProdIoc (X := X) k (k + 1) ∘ Prod.map (_root_.IicProdIoc (X := X) a k) id)
  (Function.comp (β :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    ((⇑(MeasurableEquiv.IicProdIoc (X := X) sorry) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))) → (i : ↥(Iic k.succ)) → X (↑i : ℕ)) ∘
      Prod.map id (IocProdIoc (X := X) a k (k + 1)))
    (⇑prodAssoc :
      (a_1 :
          (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) →
        ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))))
Tactic: have : (IicProdIoc (X := X) k (k + 1)) ∘ (Prod.map (IicProdIoc a k) id) =
        (IicProdIoc (h.trans k.le_succ) ∘ (Prod.map id (IocProdIoc a k (k + 1)))) ∘
        prodAssoc := by
      ext x i
      simp only [IicProdIoc_def, MeasurableEquiv.IicProdIoc, MeasurableEquiv.coe_mk,
        Equiv.coe_fn_mk, Function.comp_apply, Prod.map_fst, Prod.map_snd, id_eq,
        Nat.succ_eq_add_one, IocProdIoc]
      split_ifs <;> try rfl
      lia
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inr : partialTraj (X := X) κ a a =
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) sorry)) (_root_.IicProdIoc (X := X) a a)
Tactic: induction b, hab using Nat.le_induction with
  | base =>
    ext1 x
    rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]
    all_goals fun_prop
  | succ k h hk =>
    have : (IicProdIoc (X := X) k (k + 1)) ∘ (Prod.map (IicProdIoc a k) id) =
        (IicProdIoc (h.trans k.le_succ) ∘ (Prod.map id (IocProdIoc a k (k + 1)))) ∘
        prodAssoc := by
      ext x i
      simp only [IicProdIoc_def, MeasurableEquiv.IicProdIoc, MeasurableEquiv.coe_mk,
        Equiv.coe_fn_mk, Function.comp_apply, Prod.map_fst, Prod.map_snd, id_eq,
        Nat.succ_eq_add_one, IocProdIoc]
      split_ifs <;> try rfl
      lia
    nth_rw 1 [← partialTraj_comp_partialTraj h k.le_succ, hk, partialTraj_succ_self, comp_map,
      comap_map_comm, comap_prod, id_comap, ← id_map, map_prod_eq, ← map_comp_right, this,
      map_comp_right, id_prod_eq, prodAssoc_prod, map_comp_right, ← map_prod_map, map_id,
      ← map_comp, map_apply_eq_iff_map_symm_apply_eq, fst_prod_comp_id_prod, ← map_comp_right,
      ← coe_IicProdIoc (h.trans k.le_succ), symm_comp_self, map_id,
      deterministic_congr IicProdIoc_comp_restrict₂.symm, ← deterministic_comp_deterministic,
      comp_deterministic_eq_comap, ← comap_prod, ← map_comp, ← comp_map, ← hk,
      ← partialTraj_comp_partialTraj h k.le_succ, partialTraj_succ_self, map_comp, map_comp,
      ← map_comp_right, ← id_map, map_prod_eq, ← map_comp_right]
    · rfl
    all_goals fun_prop
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hab : a ≤ b
inr :
  partialTraj (X := X) κ a a =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a a).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a a)
⊢ partialTraj (X := X) κ a b =
    map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯)) (_root_.IicProdIoc (X := X) a b)
have inr₁ : ∀ (k : ℕ) (h : a ≤ k)
  (hk :
    partialTraj (X := X) κ a k =
      map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (partialTraj (X := X) κ a k).map (restrict₂ (π := X) sorry)) (_root_.IicProdIoc (X := X) a k)),
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (k + 1))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ map (partialTraj (X := X) κ a (k + 1)) (restrict₂ (π := X) sorry))
      (_root_.IicProdIoc (X := X) a (k + 1)))
Tactic: induction b, hab using Nat.le_induction with
  | base =>
    ext1 x
    rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]
    all_goals fun_prop
  | succ k h hk =>
    have : (IicProdIoc (X := X) k (k + 1)) ∘ (Prod.map (IicProdIoc a k) id) =
        (IicProdIoc (h.trans k.le_succ) ∘ (Prod.map id (IocProdIoc a k (k + 1)))) ∘
        prodAssoc := by
      ext x i
      simp only [IicProdIoc_def, MeasurableEquiv.IicProdIoc, MeasurableEquiv.coe_mk,
        Equiv.coe_fn_mk, Function.comp_apply, Prod.map_fst, Prod.map_snd, id_eq,
        Nat.succ_eq_add_one, IocProdIoc]
      split_ifs <;> try rfl
      lia
    nth_rw 1 [← partialTraj_comp_partialTraj h k.le_succ, hk, partialTraj_succ_self, comp_map,
      comap_map_comm, comap_prod, id_comap, ← id_map, map_prod_eq, ← map_comp_right, this,
      map_comp_right, id_prod_eq, prodAssoc_prod, map_comp_right, ← map_prod_map, map_id,
      ← map_comp, map_apply_eq_iff_map_symm_apply_eq, fst_prod_comp_id_prod, ← map_comp_right,
      ← coe_IicProdIoc (h.trans k.le_succ), symm_comp_self, map_id,
      deterministic_congr IicProdIoc_comp_restrict₂.symm, ← deterministic_comp_deterministic,
      comp_deterministic_eq_comap, ← comap_prod, ← map_comp, ← comp_map, ← hk,
      ← partialTraj_comp_partialTraj h k.le_succ, partialTraj_succ_self, map_comp, map_comp,
      ← map_comp_right, ← id_map, map_prod_eq, ← map_comp_right]
    · rfl
    all_goals fun_prop
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
have h : ∀ (x : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))),
  Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry) : ℕ))
    (((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) ∘
        _root_.IicProdIoc (X := X) a (a + 1))
      x)
    (((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
        Prod.snd)
      x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ (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
have hp : Eq.{u_1 + 1} (α :=
  ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
    X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry) : ℕ))
  ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) ∘
    _root_.IicProdIoc (X := X) a (a + 1))
  ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
    Prod.snd)
Tactic: have hp : (fun x : Π n : Iic (a + 1), X n ↦ x ⟨a + 1, mem_Iic.2 le_rfl⟩) ∘ IicProdIoc a (a + 1) =
      (piSingleton a).symm ∘ Prod.snd := by
    ext
    simp [_root_.IicProdIoc, piSingleton]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
⊢ (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
have rw : (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      (_root_.IicProdIoc (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 [partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
    ← map_comp_right _ (by fun_prop) (by fun_prop), symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
rw :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (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
⊢ (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
have rw₁ : map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) sorry)) ∘
      _root_.IicProdIoc (X := X) a (a + 1)) =
  κ a
Tactic: rw [partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
    ← map_comp_right _ (by fun_prop) (by fun_prop), symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
rw :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (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
rw₁ :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        _root_.IicProdIoc (X := X) a (a + 1)) =
    κ a
⊢ (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
have rw₂ : map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd) =
  κ a
Tactic: rw [partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
    ← map_comp_right _ (by fun_prop) (by fun_prop), symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hp :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) →
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    ((fun (x : (n : ↥(Iic (a + 1))) → X (↑n : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
      _root_.IicProdIoc (X := X) a (a + 1))
    ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
      Prod.snd)
rw :
  (map (mβ := MeasurableSpace.pi (X := fun (i : ↥(Iic (a + 1))) ↦ X (↑i : ℕ)))
      (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
        (_root_.IicProdIoc (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
rw₁ :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      ((fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯)) ∘
        _root_.IicProdIoc (X := X) a (a + 1)) =
    κ a
rw₂ :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      ((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
        Prod.snd) =
    κ a
⊢ (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
have rw₃ : map (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) (mβ := MeasurableSpace.pi (X := fun (i : ↥(Ioc a (a + 1))) ↦ X (↑i : ℕ)))
    (map (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
      Prod.snd)
    (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) =
  κ a
Tactic: rw [partialTraj_succ_self, ← map_comp_right _ (by fun_prop) (by fun_prop), hp,
    map_comp_right _ (by fun_prop) (by fun_prop), ← snd_eq, snd_prod,
    ← map_comp_right _ (by fun_prop) (by fun_prop), symm_comp_self, map_id]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inl : ∀ (hab : a ≤ b), map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) sorry) = partialTraj (X := X) κ a b
Tactic: obtain hab | hba := le_or_gt a b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
inl : ∀ (hab : a ≤ b), map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inr : ∀ (hba : b < a), map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) sorry) = partialTraj (X := X) κ a b
Tactic: obtain hab | hba := le_or_gt a b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have this : IsMarkovKernel (β := (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) (mβ :=
  MeasurableSpace.pi (X := fun (i : ↥(Ioc b (b + 1))) ↦ X (↑i : ℕ)))
  ((κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
Tactic: have := IsMarkovKernel.map (κ b) (piSingleton b).measurable
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
this :
  IsMarkovKernel (β := (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b (b + 1))) ↦ X (↑i : ℕ)))
    ((κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
have inl : Measurable.{u_1, u_1} (α := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) b (b + 1))
Tactic: rw [partialTraj_succ_eq_comp hab, map_comp, partialTraj_succ_self, ← map_comp_right,
      frestrictLe₂_comp_IicProdIoc, ← fst_eq, fst_prod, id_comp]