awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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.{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) ⋯) :
          (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
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))))
    (Kernel.id ×ₖ
      (map (mβ := Prod.instMeasurableSpace)
          (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
          (IocProdIoc (X := X) a k (k + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id) ∘ₖ
        partialTraj (X := X) κ a k))
    (Kernel.id ×ₖ
      (map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
          (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
          (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) k (k + 1)) ∘ₖ
        partialTraj (X := X) κ a k))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (β :=
    ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) ⋯) id)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a k (k + 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic k)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a k)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) k (k + 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (β := (i : ↥(Ioc a (k + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a k)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (k + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (k + 1))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic k.succ)) → X (↑i : ℕ)) (β :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ)))
    (⇑(MeasurableEquiv.symm (MeasurableEquiv.IicProdIoc (X := X) ⋯)) :
      (a_1 : (i : ↥(Iic k.succ)) → X (↑i : ℕ)) → ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ)))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    (Prod.map id (IocProdIoc (X := X) a k (k + 1)))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))) (β :=
    (i : ↥(Iic k.succ)) → X (↑i : ℕ))
    (⇑(MeasurableEquiv.IicProdIoc (X := X) ⋯) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k.succ)) → X (↑i : ℕ))) → (i : ↥(Iic k.succ)) → X (↑i : ℕ))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)
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) ⋯) :
          (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 : ℕ))))
⊢ Measurable.{u_1, u_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 : ℕ)))
    (⇑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:
fun_prop