awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
hab : a ≤ b
⊢ partialTraj (X := X) κ b b ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a b

Tactic:
simp
-- 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))
hab : a ≤ b
k : ℕ
h : b ≤ k
hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k
succ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b)
    (partialTraj (X := X) κ a (k + 1))
succ₁ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ (partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b))
    (partialTraj (X := X) κ a (k + 1))
succ₂ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ k (k + 1) ∘ₖ partialTraj (X := X) κ a k) (partialTraj (X := X) κ a (k + 1))
succ₃ succ₄ :
  Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (k + 1))
    (partialTraj (X := X) κ a (k + 1))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (partialTraj (X := X) κ b (k + 1) ∘ₖ partialTraj (X := X) κ a b) (partialTraj (X := X) κ a (k + 1))

Tactic:
rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]

Premises used: ProbabilityTheory.Kernel.comp_assoc, ProbabilityTheory.Kernel.partialTraj_succ_eq_comp, LE.le.trans
-- 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))
hab : a ≤ b
hbc : b ≤ c
base : partialTraj (X := X) κ b b ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a b
succ :
  ∀ (k : ℕ) (h : b ≤ k) (hk : partialTraj (X := X) κ b k ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a k),
    Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
      (partialTraj (X := X) κ b (k + 1) ∘ₖ partialTraj (X := X) κ a b) (partialTraj (X := X) κ a (k + 1))
⊢ partialTraj (X := X) κ b c ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a c

Tactic:
induction c, hbc using Nat.le_induction with
  | base => simp
  | succ k h hk => rw [partialTraj_succ_eq_comp h, comp_assoc, hk,
      ← partialTraj_succ_eq_comp (hab.trans h)]

Premises used: ProbabilityTheory.Kernel.comp_assoc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
h :
  ∀ (x : X) (s : Set (X × Z)) (ms : MeasurableSet s),
    Eq (α := ℝ≥0∞)
      ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
            (a : Set (X × Z)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
      ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
            (a : Set (X × Z)) → ℝ≥0∞)
          s :
        ℝ≥0∞)
⊢ deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) = Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ))

Tactic:
ext x s ms
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
mX : MeasurableSpace X
mY : MeasurableSpace Y
mZ : MeasurableSpace Z
κ : Kernel X Y
inst : IsSFiniteKernel κ
η : Kernel (X × Y) Z
inst_1 : IsSFiniteKernel η
x : X
s : Set (X × Z)
ms : MeasurableSet s
h :
  ∫⁻ (b : X × Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) b : Measure (X × Z)) : (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₁ :
  ∫⁻ (b : Y),
      (((deterministic Prod.fst ⋯ ×ₖ η : (a : X × Y) → Measure (X × Z)) (x, b) : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₂ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    (((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
        (a : Set (X × Z)) → ℝ≥0∞)
      s
h₃ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    (((η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure Z) x : Measure Z) : (a : Set Z) → ℝ≥0∞) (Prod.mk x ⁻¹' s)
h₄ :
  ∫⁻ (b : Y),
      (((η : (a : X × Y) → Measure Z) (x, b) : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(κ : (a : X) → Measure Y) x =
    ∫⁻ (b : X × Y),
      (((η : (a : X × Y) → Measure Z) b : Measure Z) : (a : Set Z) → ℝ≥0∞)
        (Prod.mk x ⁻¹' s) ∂(Kernel.id ×ₖ κ : (a : X) → Measure (X × Y)) x
⊢ Eq (α := ℝ≥0∞)
    ((((deterministic Prod.fst ⋯ ×ₖ η ∘ₖ (Kernel.id ×ₖ κ) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((Kernel.id ×ₖ (η ∘ₖ (Kernel.id ×ₖ κ)) : (a : X) → Measure (X × Z)) x : Measure (X × Z)) :
          (a : Set (X × Z)) → ℝ≥0∞)
        s :
      ℝ≥0∞)

Tactic:
simp_rw [comp_apply' _ _ _ ms, lintegral_id_prod (Kernel.measurable_coe _ ms),
    deterministic_prod_apply' _ _ _ ms, id_prod_apply' _ _ ms,
    comp_apply' _ _ _ (measurable_prodMk_left ms),
    lintegral_id_prod (η.measurable_coe (measurable_prodMk_left ms))]

Premises used: ProbabilityTheory.Kernel.lintegral_id_prod, ProbabilityTheory.Kernel.deterministic_prod_apply', ProbabilityTheory.Kernel.id_prod_apply', ProbabilityTheory.Kernel.measurable_coe, ProbabilityTheory.Kernel.comp_apply', measurable_prodMk_left
-- 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 : ℕ
inl :
  ∀ (hba : b ≤ 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)
inr :
  ∀ (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)
⊢ 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)

Tactic:
obtain hba | hab := le_total b a

Premises used: le_total
-- 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 : ℕ
hba : b ≤ a
inl :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst
inl₂ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (frestrictLe₂ (π := X) hba)
⊢ 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)

Tactic:
rw [partialTraj_le hba, IicProdIoc_le hba, map_comp_right, ← fst_eq, deterministic_map,
      fst_prod, id_map]

Premises used: ProbabilityTheory.Kernel.deterministic_map, ProbabilityTheory.Kernel.fst_prod, ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.id_map, ProbabilityTheory.Kernel.partialTraj_le, ProbabilityTheory.Kernel.fst_eq, IicProdIoc_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 : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → 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 : ℕ
hba : b ≤ a
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) Prod.fst

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

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 : ℕ
inr :
  ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)),
    Eq (α := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
      ((partialTraj (X := X) κ a a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x :
        Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
      ((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) :
            (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
          x :
        Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
⊢ 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)

Tactic:
ext1 x
-- 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 : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
inr :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a a)
inr₁ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ Eq (α := Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a a : (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
    ((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) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))
        x :
      Measure ((i : ↥(Iic a)) → X (↑i : ℕ)))

Tactic:
rw [partialTraj_self, id_map, map_apply, prod_apply, IicProdIoc_self, ← Measure.fst,
    Measure.fst_prod]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.Measure.fst_prod, ProbabilityTheory.Kernel.prod_apply, ProbabilityTheory.Kernel.id_map, ProbabilityTheory.Kernel.partialTraj_self, IicProdIoc_self, MeasureTheory.Measure.fst
-- 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 : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a a)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a a)

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 : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a)) → 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)
h₁ :
  ∀ (x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)))
    (i : ↥(Iic (k + 1))),
    (_root_.IicProdIoc (X := X) k (k + 1) ∘ Prod.map (_root_.IicProdIoc (X := X) a k) id) x i =
      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 : ℕ)))
        x i
⊢ 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:
ext x i
-- 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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : (↑i : ℕ) ≤ k
h_2 : (↑i : ℕ) ≤ a
⊢ x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑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 : ℕ)))
          x).1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)

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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : (↑i : ℕ) ≤ k
h_2 : (↑i : ℕ) ≤ a
⊢ x.1.1 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑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 : ℕ)))
          x).1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)

Tactic:
try 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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : (↑i : ℕ) ≤ k
h_2 : ¬(↑i : ℕ) ≤ a
⊢ x.1.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑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 : ℕ)))
            x).2.1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)

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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : (↑i : ℕ) ≤ k
h_2 : ¬(↑i : ℕ) ≤ a
⊢ x.1.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑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 : ℕ)))
            x).2.1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a k) (↑i : ℕ) ⋯)

Tactic:
try 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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : ¬(↑i : ℕ) ≤ k
h_2 : ¬(↑i : ℕ) ≤ a
⊢ x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑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 : ℕ)))
            x).2.2
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯)

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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : ¬(↑i : ℕ) ≤ k
h_2 : ¬(↑i : ℕ) ≤ a
⊢ x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑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 : ℕ)))
            x).2.2
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑i : ℕ) ⋯)

Tactic:
try 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)
x : (((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a k)) → X (↑i : ℕ))) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))
i : ↥(Iic (k + 1))
h_1 : ¬(↑i : ℕ) ≤ k
h_2 : (↑i : ℕ) ≤ a
⊢ x.2 (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc k (k + 1)) (↑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 : ℕ)))
          x).1
      (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (↑i : ℕ) ⋯)

Tactic:
lia