awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
pos :
  ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
neg : ∀ (h1 : i ≤ a + 1) (h2 : i ≤ a) (h3 : ¬i = a + 1), x₀ i = x₀ i
pos₁ :
  ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a) (h : i = a + 1),
    Eq.{u_1 + 1} (α := X i) (@Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ : X i)
      (Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ : X i)
neg₁ : ∀ (h1 : i ≤ a + 1) (h2 : ¬i ≤ a), ¬i = a + 1 → @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ = x₀ i
pos₂ : ∀ (h1 : ¬i ≤ a + 1) (h : i = a + 1), x₀ i = Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i ≤ a + 1 then if h : i ≤ a then x₀ i else @Eq.rec _ _ (fun (x : ℕ) (h : a + 1 = x) ↦ X x) x i ⋯ else x₀ i)
    (if h : i = a + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : a + 1 = x) ↦ X x) x ⋯ else x₀ i)
have neg₂ : ∀ (h1 : ¬i ≤ a + 1), ¬i = a + 1 → x₀ i = x₀ i
Tactic: split_ifs with h1 h2 h3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n) → ℝ≥0∞ :=
  fun (c : ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((n : ℕ) → X n)) ↦ f (updateFinset (π := X) c.2 (Iic b) c.1)
η : Kernel ((n : ℕ) → X n) ((i : ↥(Iic b)) → X (↑i : ℕ)) :=
  (partialTraj (X := X) κ a b).comap (frestrictLe (π := X) a) ⋯
⊢ Measurable (β := ℝ≥0∞) fun (x₀ : (n : ℕ) → X n) ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic b)
          z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
have change : Measurable (β := ℝ≥0∞) fun (x₀ : (n : ℕ) → X n) ↦
  ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)), g (z, x₀) ∂(η : (a : (n : ℕ) → X n) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀
Tactic: change Measurable fun x₀ ↦ ∫⁻ z : (i : Iic b) → X i, g (z, x₀) ∂η x₀
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) = lmarginalPartialTraj (X := X) κ a c f
have h : ∀ (x₀ : (n : ℕ) → X n),
  lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: ext x₀
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h : ∀ (hab : a ≤ a) (hbc : a ≤ c),
  lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: obtain rfl | hab := eq_or_lt_of_le hab
Cleared hypotheses: b, hab, hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
h :
  ∀ (hab : a ≤ a) (hbc : a ≤ c),
    lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
      lmarginalPartialTraj (X := X) κ a c f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h₁ : ∀ (hab : a < b),
  lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: obtain rfl | hab := eq_or_lt_of_le hab
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc : a ≤ c
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h : ∀ (hbc : a ≤ a),
  lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a a f) x₀ =
    lmarginalPartialTraj (X := X) κ a a f x₀
Tactic: obtain rfl | hbc := eq_or_lt_of_le hbc
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc : a ≤ c
h :
  ∀ (hbc : a ≤ a),
    lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a a f) x₀ =
      lmarginalPartialTraj (X := X) κ a a f x₀
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h₁ : ∀ (hbc : a < c),
  lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: obtain rfl | hbc := eq_or_lt_of_le hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h : ∀ (hbc : b ≤ b),
  lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b b f) x₀ =
    lmarginalPartialTraj (X := X) κ a b f x₀
Tactic: obtain rfl | hbc := eq_or_lt_of_le hbc
Cleared hypotheses: c, hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
h :
  ∀ (hbc : b ≤ b),
    lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b b f) x₀ =
      lmarginalPartialTraj (X := X) κ a b f x₀
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h₁ : ∀ (hbc : b < c),
  lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: obtain rfl | hbc := eq_or_lt_of_le hbc
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab hbc : a ≤ a
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a a f) x₀ =
    lmarginalPartialTraj (X := X) κ a a f x₀
have h : lmarginalPartialTraj (X := X) κ a a f x₀ = lmarginalPartialTraj (X := X) κ a a f x₀
Tactic: rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a ≤ a
hbc_1 : a ≤ c
hbc : a < c
⊢ lmarginalPartialTraj (X := X) κ a a (lmarginalPartialTraj (X := X) κ a c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h : lmarginalPartialTraj (X := X) κ a c f x₀ = lmarginalPartialTraj (X := X) κ a c f x₀
Tactic: rw [lmarginalPartialTraj_le κ le_rfl (measurable_lmarginalPartialTraj _ _ hf)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b ≤ b
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b b f) x₀ =
    lmarginalPartialTraj (X := X) κ a b f x₀
have h : lmarginalPartialTraj (X := X) κ a b f x₀ = lmarginalPartialTraj (X := X) κ a b f x₀
Tactic: rw [lmarginalPartialTraj_le κ le_rfl hf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc_1 : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ lmarginalPartialTraj (X := X) κ a b (lmarginalPartialTraj (X := X) κ b c f) x₀ =
    lmarginalPartialTraj (X := X) κ a c f x₀
have h : ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
    ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic c)
          z) ∂(partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        z ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
      ((Iic a).restrict (π := X) x₀) =
  ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
    f
      (updateFinset (π := X) x₀ (Iic c)
        z) ∂(partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
      ((Iic a).restrict (π := X) x₀)
Tactic: simp_rw [lmarginalPartialTraj, frestrictLe, restrict_updateFinset,
    updateFinset_updateFinset_of_subset (Iic_subset_Iic.2 hbc.le)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab_1 : a ≤ b
hbc_1 : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
        f
          (updateFinset (π := X) x₀ (Iic c)
            z) ∂(partialTraj (X := X) κ b c : (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
          z ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X (↑i : ℕ)),
      f
        (updateFinset (π := X) x₀ (Iic c)
          z) ∂(partialTraj (X := X) κ a c : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic c)) → X (↑i : ℕ)))
        ((Iic a).restrict (π := X) x₀)
have h : Measurable (β := ℝ≥0∞) fun (z : (i : ↥(Iic c)) → X (↑i : ℕ)) ↦ f (updateFinset (π := X) x₀ (Iic c) z)
Tactic: rw [← lintegral_comp, partialTraj_comp_partialTraj hab.le hbc.le]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
⊢ lmarginalPartialTraj (X := X) κ b c f = f
have h : ∀ (x : (n : ℕ) → X n), lmarginalPartialTraj (X := X) κ b c f x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ lmarginalPartialTraj (X := X) κ b c f x = f x
have h : ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
    f
      (Function.updateFinset (π := X) x (Ioc b c)
        x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) sorry) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x) =
  f x
Tactic: rw [lmarginalPartialTraj_eq_lintegral_map mf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc b c)
          x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
          (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x) =
    f x
have h : IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
  MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
  (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) sorry) :
      (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
    (frestrictLe (π := X) b x))
Tactic: refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
h :
  IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x))
⊢ ∫⁻ (x_1 : (i : ↥(Ioc b c)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc b c)
          x_1) ∂((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
          (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
        (frestrictLe (π := X) b x) =
    f x
have h₁ : ∀ (y : (i : ↥(Ioc b c)) → X (↑i : ℕ)) (i : ℕ) (hi : i ∈ (↑(Iic a) : Set ℕ)),
  Function.updateFinset (π := X) x (Ioc b c) y i = x i
Tactic: refine @lintegral_eq_const _ _ _ ?_ _ _ (ae_of_all _ fun y ↦ hf fun i hi ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsProbabilityMeasure.{u_1} (α := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (m0 :=
    MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
    (((partialTraj (X := X) κ b c).map (restrict₂ (π := X) ⋯) :
        (a : (i : ↥(Iic b)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc b c)) → X (↑i : ℕ)))
      (frestrictLe (π := X) b x))
have h : IsMarkovKernel (β := (i : ↥(Ioc b c)) → X (↑i : ℕ)) (mβ := MeasurableSpace.pi (X := fun (i : ↥(Ioc b c)) ↦ X (↑i : ℕ)))
  ((partialTraj (X := X) κ b c).map (restrict₂ (π := X) sorry))
Tactic: refine @IsMarkovKernel.isProbabilityMeasure _ _ _ _ _ ?_ _
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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 : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hab : a ≤ b
x : (n : ℕ) → X n
y : (i : ↥(Ioc b c)) → X (↑i : ℕ)
i : ℕ
hi : i ∈ (↑(Iic a) : Set ℕ)
⊢ Function.updateFinset (π := X) x (Ioc b c) y i = x i
have h : ∀ (hf : DependsOn (α := X) f (Set.Iic a)) (hab : a ≤ b) (hi : i ≤ a) (h : b < i ∧ i ≤ c),
  y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc b c) i sorry) = x i
Tactic: simp_all only [coe_Iic, Set.mem_Iic, Function.updateFinset, mem_Ioc, dite_eq_right_iff]
Cleared hypotheses: hf, hab, hi
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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)
d : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hac : a ≤ c
had : a ≤ d
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inr : ∀
  (this :
    ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
      lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f)
  (hcd : ¬c ≤ d), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
Tactic: wlog hcd : c ≤ d generalizing c d
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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)
d : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hac : a ≤ c
had : a ≤ d
inr :
  ∀
    (this :
      ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
        lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f)
    (hcd : ¬c ≤ d), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have wlog : ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
  lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
Tactic: wlog hcd : c ≤ d generalizing c d
Cleared hypotheses: d, hac, had
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
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)
d : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
hac : a ≤ c
had : a ≤ d
this :
  ∀ {c d : ℕ} (hac : a ≤ c) (had : a ≤ d) (hcd : c ≤ d),
    lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
hcd : ¬c ≤ d
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inr : lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c f
Tactic: rw [this had hac (le_of_not_ge hcd)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inl : ∀ (hbc : b ≤ c), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
Tactic: obtain hbc | hcb := le_total b c
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
inl : ∀ (hbc : b ≤ c), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inr : ∀ (hcb : c ≤ b), lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
Tactic: obtain hbc | hcb := le_total b c
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hbc : b ≤ c
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inl : lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c (lmarginalPartialTraj (X := X) κ c d f)
Tactic: rw [← lmarginalPartialTraj_self hbc hcd mf, hf.lmarginalPartialTraj_of_le d mf hac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hbc : b ≤ c
inl :
  lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c (lmarginalPartialTraj (X := X) κ c d f)
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inl₁ : lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b c f
Tactic: rw [← lmarginalPartialTraj_self hbc hcd mf, hf.lmarginalPartialTraj_of_le d mf hac]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inr : f = lmarginalPartialTraj (X := X) κ b d f
Tactic: rw [hf.lmarginalPartialTraj_of_le c mf (hac.trans hcb),
      hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
inr : f = lmarginalPartialTraj (X := X) κ b d f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f
have inr₁ : f = f
Tactic: rw [hf.lmarginalPartialTraj_of_le c mf (hac.trans hcb),
      hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
have inl : ∀ (hba : b ≤ a), lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
Tactic: obtain hba | hab := le_total b a