awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
k : ℕ
hk : n ≤ k
h :
  Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x)
h₁ :
  Eq (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((η.map (frestrictLe (π := X) k) : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
h₂ h₃ :
  Eq (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    ((partialTraj (X := X) κ a k : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic k)) → X (↑i : ℕ))) x :
      Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
⊢ Eq.{u_1 + 1} (α := Measure ((i : ↥(Iic k)) → X (↑i : ℕ)))
    (Measure.map (frestrictLe (π := X) k) ((η : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    (inducedFamily (X := X)
      (fun (n : ℕ) ↦
        (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)
      (Iic k))

Tactic:
rw [inducedFamily_Iic, ← map_apply _ (measurable_frestrictLe k), hη k hk]

Premises used: ProbabilityTheory.Kernel.map_apply, MeasureTheory.inducedFamily_Iic, Preorder.measurable_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveMeasureFamily (α := X)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)

Tactic:
isProjectiveMeasureFamily_partialTraj κ x

Premises used: ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
x : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveMeasureFamily (α := X)
    (inducedFamily (X := X) fun (n : ℕ) ↦
      (partialTraj (X := X) κ a n : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) x)

Tactic:
exact isProjectiveMeasureFamily_partialTraj κ x

Premises used: ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
η : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((n : ℕ) → X n)
hη : ∀ (b : ℕ), η.map (frestrictLe (π := X) b) = partialTraj (X := X) κ a b
⊢ η = traj (X := X) κ a

Tactic:
eq_traj' κ 0 η fun b _ ↦ hη b

Premises used: ProbabilityTheory.Kernel.eq_traj', OfNat.ofNat
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
⊢ traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b = traj (X := X) κ a

Tactic:
eq_traj _ _ fun n ↦ ?_

Premises used: ProbabilityTheory.Kernel.eq_traj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
refine :
  ∀ (n : ℕ), (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n
⊢ traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b = traj (X := X) κ a

Tactic:
refine eq_traj _ _ fun n ↦ ?_

Premises used: ProbabilityTheory.Kernel.eq_traj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
n : ℕ
rw : (traj (X := X) κ b).map (frestrictLe (π := X) n) ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
rw₁ : partialTraj (X := X) κ b n ∘ₖ partialTraj (X := X) κ a b = partialTraj (X := X) κ a n
rw₂ rw₃ : partialTraj (X := X) κ a n = partialTraj (X := X) κ a n
⊢ (traj (X := X) κ b ∘ₖ partialTraj (X := X) κ a b).map (frestrictLe (π := X) n) = partialTraj (X := X) κ a n

Tactic:
rw [map_comp, traj_map_frestrictLe, partialTraj_comp_partialTraj' _ hab]

Premises used: ProbabilityTheory.Kernel.partialTraj_comp_partialTraj', ProbabilityTheory.Kernel.map_comp, ProbabilityTheory.Kernel.traj_map_frestrictLe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
⊢ traj (X := X) κ a =
    map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
(eq_traj' _ (a + 1) _ fun b hb ↦ ?_).symm

Premises used: ProbabilityTheory.Kernel.eq_traj', HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
refine :
  ∀ (b : ℕ) (hb : b ≥ a + 1),
    map (mβ := MeasurableSpace.pi (X := X))
        (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
          (⇑(IicProdIoi (X := X) a) :
            (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
        (frestrictLe (π := X) b) =
      partialTraj (X := X) κ a b
⊢ traj (X := X) κ a =
    map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
refine (eq_traj' _ (a + 1) _ fun b hb ↦ ?_).symm

Premises used: ProbabilityTheory.Kernel.eq_traj', HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
rw :
  map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (frestrictLe (π := X) b ∘
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)) =
    partialTraj (X := X) κ a b
hf :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
hg : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
⊢ map (mβ := MeasurableSpace.pi (X := X))
      (map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))
      (frestrictLe (π := X) b) =
    partialTraj (X := X) κ a b

Tactic:
rw [← map_comp_right]

Premises used: ProbabilityTheory.Kernel.map_comp_right
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
enter :
  frestrictLe (π := X) b ∘
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)
| map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
    (frestrictLe (π := X) b ∘
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))

Tactic:
enter [2]
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
change :
  Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
    (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))
| frestrictLe (π := X) b ∘
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).1⟩))

Premises used: id, Prod.map, IicProdIoc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
enter :
  Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (_root_.IicProdIoc (X := X) a b)
    (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))
| map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
    (frestrictLe (π := X) b ∘
      (⇑(IicProdIoi (X := X) a) :
        (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n))

Tactic:
enter [2]; change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).1⟩))

Premises used: id, Prod.map, IicProdIoc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
conv_lhs :
  map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (frestrictLe (π := X) b ∘
        (⇑(IicProdIoi (X := X) a) :
          (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)) =
    partialTraj (X := X) κ a b

Tactic:
conv_lhs => enter [2]; change (IicProdIoc a b) ∘
    (Prod.map id (fun x i ↦ x ⟨i.1, Set.mem_Ioi.2 (mem_Ioc.1 i.2).1⟩))

Premises used: id, Prod.map, IicProdIoc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
rw :
  map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))
hg :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₁ : MeasurableSpace ((i : ↥(Ioc a b)) → X (↑i : ℕ))
hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id
hg₁ :
  Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)
rw₂ : MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))
hf₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))
hg₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b)
⊢ map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ a).map ((Set.Ioi a).restrict (π := X)))
      (Function.comp (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (_root_.IicProdIoc (X := X) a b)
        (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))) =
    partialTraj (X := X) κ a b

Tactic:
rw [map_comp_right, ← map_prod_map, ← map_comp_right]

Premises used: ProbabilityTheory.Kernel.map_comp_right, ProbabilityTheory.Kernel.map_prod_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
enter :
  (fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
    (Set.Ioi a).restrict (π := X)
| map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (map Kernel.id id ×ₖ
      (traj (X := X) κ a).map
        ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
          (Set.Ioi a).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b)

Tactic:
enter [1, 2, 2]
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
change : (Ioc a b).restrict (π := X)
| (fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
    (Set.Ioi a).restrict (π := X)

Tactic:
change (Ioc a b).restrict

Premises used: Finset.restrict, Finset.Ioc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
enter : (Ioc a b).restrict (π := X)
| map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
    (map Kernel.id id ×ₖ
      (traj (X := X) κ a).map
        ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
          (Set.Ioi a).restrict (π := X)))
    (_root_.IicProdIoc (X := X) a b)

Tactic:
enter [1, 2, 2]; change (Ioc a b).restrict

Premises used: Finset.restrict, Finset.Ioc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
conv_lhs :
  map (mβ := Prod.instMeasurableSpace) (map Kernel.id id ×ₖ (traj (X := X) κ a).map ((Ioc a b).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)
      (map Kernel.id id ×ₖ
        (traj (X := X) κ a).map
          ((fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
              x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)) ∘
            (Set.Ioi a).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b

Tactic:
conv_lhs => enter [1, 2, 2]; change (Ioc a b).restrict

Premises used: Finset.restrict, Finset.Ioc
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
hf : Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)
hg :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic b)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a b)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ map (mβ := Prod.instMeasurableSpace) (map Kernel.id id ×ₖ (traj (X := X) κ a).map ((Ioc a b).restrict (π := X)))
      (_root_.IicProdIoc (X := X) a b) =
    partialTraj (X := X) κ a b

Tactic:
rw [← restrict₂_comp_restrict Ioc_subset_Iic_self, ← frestrictLe, map_comp_right,
        traj_map_frestrictLe, map_id, ← partialTraj_eq_prod]

Premises used: ProbabilityTheory.Kernel.map_comp_right, Finset.Ioc_subset_Iic_self, Finset.restrict₂_comp_restrict, ProbabilityTheory.Kernel.traj_map_frestrictLe, Preorder.frestrictLe, ProbabilityTheory.Kernel.partialTraj_eq_prod, ProbabilityTheory.Kernel.map_id
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) (β := (i : ↥(Iic b)) → X (↑i : ℕ)) (frestrictLe (π := X) b)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ 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.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := (n : ℕ) → X n) ((Set.Ioi a).restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable (β := (i : ↥(Ioc a b)) → X (↑i : ℕ))
    fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
    x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) id

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Prod.map id fun (x : (a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ)) (i : ↥(Ioc a b)) ↦
      x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Set.Ioi a) (↑i : ℕ) ⋯))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a b)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hb : b ≥ a + 1
⊢ Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((a_1 : (↑(Set.Ioi a) : Type)) → X (↑a_1 : ℕ))) (β :=
    (n : ℕ) → X n)
    (⇑(IicProdIoi (X := X) a) :
      (a : ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi a) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
n : ℕ
x : (i : ↥(Iic n)) → X (↑i : ℕ)
nth_rw :
  Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((map (mβ := Prod.instMeasurableSpace) (Kernel.id ×ₖ (traj (X := X) κ n).map ((Set.Ioi n).restrict (π := X)))
          (⇑(IicProdIoi (X := X) n) :
            (a : ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : (↑(Set.Ioi n) : Type)) → X (↑i : ℕ))) → (n : ℕ) → X n) :
        (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n))
      x)
⊢ Eq.{u_1 + 1} (α := Measure ((i : ℕ) → X i))
    (Measure.map (fun (x_1 : (i : ℕ) → X i) ↦ updateFinset (π := X) x_1 (Iic n) x)
      ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x))
    ((traj (X := X) κ n : (a : (i : ↥(Iic n)) → X (↑i : ℕ)) → Measure ((n : ℕ) → X n)) x)

Tactic:
nth_rw 2 [traj_eq_prod]

Premises used: ProbabilityTheory.Kernel.traj_eq_prod