awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₁ : n ≤ n + 1
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
  (IocProdIoc (X := X) a n (n + 1))
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₃ : Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₅ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (β :=
  ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) sorry) id)
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
inl₅ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (β :=
    ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) ⋯) id)
inl₆ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₇ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) n (n + 1))
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
inl₅ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (β :=
    ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) ⋯) id)
inl₆ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₇ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) n (n + 1))
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₈ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (n + 1))) → X (↑i : ℕ)) (β := (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
  (restrict₂ (π := X) sorry)
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
n : ℕ
hn : a.succ ≤ n
hind :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a n)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a n)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
this :
  Eq.{u_1 + 1} (α :=
    ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) → (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) n (n + 1))
    (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) ⋯) id)
inl : a ≤ n
inl₁ : n ≤ n + 1
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
inl₄ : Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id
inl₅ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (β :=
    ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) (Prod.map (restrict₂ (π := X) ⋯) id)
inl₆ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Ioc a n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (IocProdIoc (X := X) a n (n + 1))
inl₇ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic n)) → X (↑i : ℕ)) × ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) n (n + 1))
inl₈ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic (n + 1))) → X (↑i : ℕ)) (β := (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)
⊢ Eq (α := Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a (n + 1))
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a (n + 1))) → X (↑i : ℕ)))
have inl₉ : Measurable.{u_1, u_1} (α := X (n + 1)) (β := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
  (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
Tactic: rw [const_apply, partialTraj_succ_of_le (by lia), map_const, prod_const_comp, id_comp,
        ← map_comp_right, this, map_comp_right, ← map_prod_map, hind, Kernel.map_id, map_apply,
        prod_apply, const_apply, const_apply, Measure.map_piSingleton,
        Measure.pi_prod_map_IocProdIoc]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
have this : IsEmpty ↥(Ioc a b)
Tactic: have : IsEmpty (Ioc a b) := by simpa [hba] using Subtype.isEmpty_false
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
have inr : ∀ (x : (i : ↥(Iic a)) → X (↑i : ℕ)) (s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) (ms : MeasurableSet s),
  Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) sorry) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: ext x s ms
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hba : b ≤ a
this : IsEmpty ↥(Ioc a b)
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))
ms : MeasurableSet s
⊢ Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) ⋯) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
have pos : ∀ (hs : s.Nonempty),
  Eq (α := ℝ≥0∞)
    ((((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a b)
                  (restrict₂ (π := X) sorry) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
    ((((const ((i : ↥(Iic a)) → X (↑i : ℕ))
                  (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)) :
                (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
              x :
            Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc a b)) → X (↑i : ℕ))) → ℝ≥0∞)
        s :
      ℝ≥0∞)
Tactic: by_cases hs : s.Nonempty