awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (hypothesis)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
⊢ Eq (α := ℝ≥0∞)
    (((map (α := X (n + 1)) (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
              (μ (n + 1)) :
            Measure ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Ioc n (n + 1)), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have this : Subsingleton ↥(Ioc n (n + 1))
Tactic: have : Subsingleton (Ioc n (n + 1)) := by rw [Nat.Ioc_succ_singleton]; infer_instance
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ Eq (α := ℝ≥0∞)
    (((map (α := X (n + 1)) (⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))
              (μ (n + 1)) :
            Measure ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Ioc n (n + 1))) → X (↑i : ℕ))) → ℝ≥0∞)
        (Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (∏ i : ↥(Ioc n (n + 1)), ((μ (↑i : ℕ) : Measure (X (↑i : ℕ))) : (a : Set (X (↑i : ℕ))) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞)
  (((μ (n + 1) : Measure (X (n + 1))) : (a : Set (X (n + 1))) → ℝ≥0∞)
      ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
        Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
    ℝ≥0∞)
  (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) : ℕ) :
          Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) : ℕ))) :
        (a : Set (X (↑⟨n + 1, sorry⟩ : ℕ))) → ℝ≥0∞)
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry)) :
    ℝ≥0∞)
Tactic: rw [Fintype.prod_subsingleton _ ⟨n + 1, mem_Ioc.2 (by lia)⟩,
    Measure.map_apply (by fun_prop) (.univ_pi hs)]
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
⊢ Eq (α := ℝ≥0∞)
    (((μ (n + 1) : Measure (X (n + 1))) : (a : Set (X (n + 1))) → ℝ≥0∞)
        ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
          Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s) :
      ℝ≥0∞)
    (((μ (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ) :
            Measure (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ))) :
          (a : Set (X (↑⟨n + 1, ⋯⟩ : ℕ))) → ℝ≥0∞)
        (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯)) :
      ℝ≥0∞)
have h : ∀ (x : X (n + 1)),
  Membership.mem (γ := Set (X (n + 1)))
      ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
        Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s)
      x ↔
    Membership.mem (γ := Set (X (n + 1)))
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) :
        Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) : ℕ)))
      x
Tactic: congr 1 with x
-- Lean 4 proof step from Mathlib.Probability.ProductMeasure (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X (↑i : ℕ))
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
this : Subsingleton ↥(Ioc n (n + 1))
x : X (n + 1)
⊢ Membership.mem (γ := Set (X (n + 1)))
      ((⇑(piSingleton (X := X) n) : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) ⁻¹'
        Set.pi (α := fun (i : ↥(Ioc n (n + 1))) ↦ X (↑i : ℕ)) Set.univ s)
      x ↔
    Membership.mem (γ := Set (X (n + 1)))
      (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ)))
      x
have h : (∀ (a : ℕ) (b : a = n + 1),
    Membership.mem (α := X a) (γ := Set (X a))
      (s (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a sorry) :
        Set (X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a sorry) : ℕ)))
      ((piSingleton (X := X) n : (a : X (n + 1)) → (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) x
          (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a sorry) :
        X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a sorry) : ℕ))) ↔
  Membership.mem (γ := Set (X (n + 1)))
    (s (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) :
      Set (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc n (n + 1)) (n + 1) sorry) : ℕ)))
    x
Tactic: simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, forall_const, Subtype.forall,
    Nat.Ioc_succ_singleton, mem_singleton]
-- 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 : ℕ
⊢ 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 inl : ∀ (hab : 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) sorry))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
Tactic: obtain hab | hba := lt_or_ge a b
-- 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 : ℕ
inl :
  ∀ (hab : 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 : ℕ)))
⊢ 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 : ∀ (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) sorry))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a b)) ↦ μ (↑i : ℕ)))
Tactic: obtain hab | hba := lt_or_ge a b
-- 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
⊢ 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 inl : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
  (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
    (restrict₂ (π := X) sorry))
  (const ((i : ↥(Iic a)) → X (↑i : ℕ))
    (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)))
Tactic: refine Nat.le_induction ?_ (fun n hn hind ↦ ?_) b (Nat.succ_le_of_lt hab)
-- 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
inl :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)))
⊢ 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 inl₁ : ∀ (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) sorry))
      (const ((i : ↥(Iic a)) → X (↑i : ℕ))
        (Measure.pi (α := fun (i : ↥(Ioc a n)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a n)) ↦ μ (↑i : ℕ)))),
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((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) sorry))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)))
Tactic: refine Nat.le_induction ?_ (fun n hn hind ↦ ?_) b (Nat.succ_le_of_lt hab)
-- 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
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    (Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
      (restrict₂ (π := X) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)))
have inl : ∀ (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)),
  Eq (α := Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
            (restrict₂ (π := X) sorry) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
Tactic: ext1 x₀
-- 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 : ℕ)))
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((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) ⋯))
    (const ((i : ↥(Iic a)) → X (↑i : ℕ))
      (Measure.pi (α := fun (i : ↥(Ioc a (n + 1))) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a (n + 1))) ↦ μ (↑i : ℕ)))
have inl : ∀ (x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)),
  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) sorry) :
          (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 : ℕ)))
Tactic: ext1 x₀
-- 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
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ Eq (α := Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
have inl : Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
  (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
Tactic: rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply,
        const_apply, Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod,
        measure_univ, one_smul]
-- 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
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
inl :
  Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
⊢ Eq (α := Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
have inl₁ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (β :=
  (i : ↥(Ioc a a.succ)) → X (↑i : ℕ)) (restrict₂ (π := X) sorry ∘ _root_.IicProdIoc (X := X) a (a + 1))
Tactic: rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply,
        const_apply, Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod,
        measure_univ, one_smul]
-- 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
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
inl :
  Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
inl₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (β :=
    (i : ↥(Ioc a a.succ)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) a (a + 1))
⊢ Eq (α := Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
have inl₂ : Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
  (_root_.IicProdIoc (X := X) a (a + 1))
Tactic: rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply,
        const_apply, Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod,
        measure_univ, one_smul]
-- 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
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
inl :
  Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
inl₁ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (β :=
    (i : ↥(Ioc a a.succ)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯ ∘ _root_.IicProdIoc (X := X) a (a + 1))
inl₂ :
  Measurable.{u_1, u_1} (α := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)))
    (_root_.IicProdIoc (X := X) a (a + 1))
⊢ Eq (α := Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((Kernel.map (partialTraj (X := X) (fun (n : ℕ) ↦ const ((i : ↥(Iic n)) → X (↑i : ℕ)) (μ (n + 1))) a a.succ)
            (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
    ((const ((i : ↥(Iic a)) → X (↑i : ℕ))
            (Measure.pi (α := fun (i : ↥(Ioc a a.succ)) ↦ X (↑i : ℕ)) fun (i : ↥(Ioc a a.succ)) ↦ μ (↑i : ℕ)) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
        x₀ :
      Measure ((i : ↥(Ioc a a.succ)) → X (↑i : ℕ)))
have inl₃ : Measurable.{u_1, u_1} (α := (i : ↥(Iic a.succ)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a.succ)) → X (↑i : ℕ))
  (restrict₂ (π := X) sorry)
Tactic: rw [partialTraj_succ_self, ← map_comp_right, map_apply, prod_apply, map_apply, const_apply,
        const_apply, Measure.map_piSingleton, restrict₂_comp_IicProdIoc, Measure.map_snd_prod,
        measure_univ, one_smul]
-- 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 : ℕ
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 : ℕ)
⊢ 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 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) sorry ∘ _root_.IicProdIoc (X := X) n (n + 1))
  (IocProdIoc (X := X) a n (n + 1) ∘ Prod.map (restrict₂ (π := X) sorry) id)
Tactic: have : (restrict₂ (Ioc_subset_Iic_self (a := a))) ∘ (IicProdIoc (X := X) n (n + 1)) =
          (IocProdIoc a n (n + 1)) ∘ (Prod.map (restrict₂ Ioc_subset_Iic_self) id) := rfl
-- 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)
⊢ 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 : a ≤ n
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]