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)
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 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 : ℕ)) ∘
      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)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    (Prod.map (_root_.IicProdIoc (X := X) a k) 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 : ℕ), IsMarkovKernel (κ n)
a : ℕ
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) ⋯) : ℕ))
      (((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))
        x)
      (((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
          Prod.snd)
        x)
⊢ 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)

Tactic:
ext
-- 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 : ℕ), IsMarkovKernel (κ n)
a : ℕ
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) ⋯) : ℕ))
    (((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))
      x)
    (((⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 1)) ∘
        Prod.snd)
      x)

Tactic:
simp [_root_.IicProdIoc, piSingleton]

Premises used: IicProdIoc, MeasurableEquiv.piSingleton
-- 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 : ℕ), 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)

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]
-- 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 : ℕ), 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)
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 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 : ℕ), 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)
⊢ Measurable (β := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    fun (x : (i : ↥(Iic (a + 1))) → X (↑i : ℕ)) ↦ x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 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 : ℕ), 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)
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) Prod.snd

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 : ℕ), 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)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) (β :=
    X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic (a + 1)) (a + 1) ⋯) : ℕ))
    (⇑(MeasurableEquiv.symm (piSingleton (X := X) a)) : (a_1 : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) → X (a + 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 : ℕ), 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)
⊢ Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → 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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
inl : ∀ (hab : a ≤ b), map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
inr : ∀ (hba : b < a), 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

Tactic:
obtain hab | hba := le_or_gt a b

Premises used: le_or_gt
-- 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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ 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
-- 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 : ℕ), 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 : ℕ)))
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))
inl₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b

Tactic:
rw [partialTraj_succ_eq_comp hab, map_comp, partialTraj_succ_self, ← map_comp_right,
      frestrictLe₂_comp_IicProdIoc, ← fst_eq, fst_prod, id_comp]

Premises used: ProbabilityTheory.Kernel.fst_prod, ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, ProbabilityTheory.Kernel.partialTraj_succ_self, ProbabilityTheory.Kernel.fst_eq, ProbabilityTheory.Kernel.map_comp, ProbabilityTheory.Kernel.id_comp, frestrictLe₂_comp_IicProdIoc
-- 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 : ℕ), 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 : ℕ)))
⊢ 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:
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 : ℕ), 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 : ℕ)))
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := 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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
inr :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯ ∘ frestrictLe₂ (π := X) ⋯) ⋯) (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)
inr₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)
⊢ map (partialTraj (X := X) κ a (b + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b

Tactic:
rw [partialTraj_le (Nat.succ_le_of_lt hba), partialTraj_le hba.le, deterministic_map]

Premises used: ProbabilityTheory.Kernel.deterministic_map, Nat.succ_le_of_lt, LT.lt.le, ProbabilityTheory.Kernel.partialTraj_le
-- 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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯ ∘ frestrictLe₂ (π := X) ⋯) ⋯) (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)

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 : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hba : b < a
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (b + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b

Tactic:
map_id ..

Premises used: Preorder.frestrictLe₂, Finset.restrict₂, ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b

Tactic:
exact map_id ..

Premises used: ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a k : ℕ
h : b ≤ k
hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b
succ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)
succ₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic k)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) h)
⊢ map (partialTraj (X := X) κ a (k + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b

Tactic:
rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]

Premises used: ProbabilityTheory.Kernel.map_comp_right, Nat.le_succ, ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂, Preorder.frestrictLe₂_comp_frestrictLe₂
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a k : ℕ
h : b ≤ k
hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (frestrictLe₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a k : ℕ
h : b ≤ k
hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic k)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) h)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hbc : b ≤ c
base : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
succ :
  ∀ (k : ℕ) (h : b ≤ k) (hk : (partialTraj (X := X) κ a k).map (frestrictLe₂ (π := X) h) = partialTraj (X := X) κ a b),
    map (partialTraj (X := X) κ a (k + 1)) (frestrictLe₂ (π := X) ⋯) = partialTraj (X := X) κ a b
⊢ (partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) = partialTraj (X := X) κ a b

Tactic:
induction c, hbc using Nat.le_induction with
  | base => exact map_id ..
  | succ k h hk =>
    rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
    all_goals fun_prop

Premises used: ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.partialTraj_succ_map_frestrictLe₂, ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hbc : b ≤ c
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic c)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hbc)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
hbc : b ≤ c
rw :
  Eq (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (((partialTraj (X := X) κ a c).map (frestrictLe₂ (π := X) hbc) :
          (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 : ℕ)))
rw₁ 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 : ℕ)))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe₂ (π := X) hbc)
      ((partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ))) x₀))
    ((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)

Tactic:
rw [← map_apply _ (by fun_prop), partialTraj_map_frestrictLe₂]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
inl : ∀ (hbc : b ≤ c), partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
inr : ∀ (hcb : c ≤ b), partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c

Tactic:
obtain hbc | hcb := le_total b c

Premises used: le_total
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hbc : b ≤ c
inl inl₁ : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c

Tactic:
rw [partialTraj_comp_partialTraj hab hbc]

Premises used: ProbabilityTheory.Kernel.partialTraj_comp_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
hab : a ≤ b
hcb : c ≤ b
inr : deterministic (frestrictLe₂ (π := X) hcb) ⋯ ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c
inr₁ : (partialTraj (X := X) κ a b).map (frestrictLe₂ (π := X) hcb) = partialTraj (X := X) κ a c
inr₂ inr₃ : partialTraj (X := X) κ a c = partialTraj (X := X) κ a c
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c

Tactic:
rw [partialTraj_le hcb, deterministic_comp_eq_map, partialTraj_map_frestrictLe₂]

Premises used: ProbabilityTheory.Kernel.deterministic_comp_eq_map, ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂