awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.ProductMeasure
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)
h :
  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
b : n + 1 = n + 1
⊢ Membership.mem (α := X (n + 1)) (γ := Set (X (n + 1)))
    (s (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) (n + 1) ⋯) :
      Set (X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ)))
    ((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)) (n + 1) ⋯) :
      X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) (n + 1) ⋯) : ℕ))

Tactic:
h

Premises used: Set.Mem
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ (∀ (a : ℕ) (b : a = n + 1),
      Membership.mem (α := X a) (γ := Set (X a))
        (s (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) :
          Set (X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ)))
        ((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 ⋯) :
          X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ))) ↔
    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

Tactic:
⟨fun h ↦ h (n + 1) rfl, fun h a b ↦ b.symm ▸ h⟩

Premises used: HAdd.hAdd, Iff.intro, OfNat.ofNat, Eq.symm, rfl
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ (∀ (a : ℕ) (b : a = n + 1),
      Membership.mem (α := X a) (γ := Set (X a))
        (s (Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) :
          Set (X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ)))
        ((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 ⋯) :
          X (↑(Subtype.mk (p := fun (a : ℕ) ↦ a ∈ Ioc n (n + 1)) a ⋯) : ℕ))) ↔
    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

Tactic:
exact ⟨fun h ↦ h (n + 1) rfl, fun h a b ↦ b.symm ▸ h⟩
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)))
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) ⋯))
      (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 : ℕ)))

Tactic:
obtain hab | hba := lt_or_ge a b

Premises used: lt_or_ge
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)))

Tactic:
Nat.le_induction ?_ (fun n hn hind ↦ ?_) b (Nat.succ_le_of_lt hab)

Premises used: Nat.succ_le_of_lt, Nat.le_induction
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)))
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) ⋯))
        (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 : ℕ)))
⊢ 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 : ℕ)))

Tactic:
refine Nat.le_induction ?_ (fun n hn hind ↦ ?_) b (Nat.succ_le_of_lt hab)
-- Module: Mathlib.Probability.ProductMeasure
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
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) ⋯) :
            (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 : ℕ)))
⊢ 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 : ℕ)))

Tactic:
ext1 x₀
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)))
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) ⋯) :
            (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 : ℕ)))
⊢ 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 : ℕ)))

Tactic:
ext1 x₀
-- Module: Mathlib.Probability.ProductMeasure
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))
inl₃ :
  Measurable.{u_1, u_1} (α := (i : ↥(Iic a.succ)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a.succ)) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)
⊢ 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 : ℕ)))

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]

Premises used: ProbabilityTheory.Kernel.map_apply, ProbabilityTheory.Kernel.map_comp_right, MeasureTheory.Measure.map_piSingleton, ProbabilityTheory.Kernel.prod_apply, MeasureTheory.IsProbabilityMeasure.measure_univ, ProbabilityTheory.Kernel.partialTraj_succ_self, one_smul, ProbabilityTheory.Kernel.const_apply, MeasureTheory.Measure.map_snd_prod, restrict₂_comp_IicProdIoc
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)
⊢ 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:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)
⊢ 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))

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)
⊢ 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:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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 : ℕ)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic a.succ)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a a.succ)) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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.{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)

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
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ a ≤ n

Tactic:
lia
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ 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:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic n)) → X (↑i : ℕ)) (β := (i : ↥(Ioc a n)) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Ioc n (n + 1))) → X (↑i : ℕ)) id

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ 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)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ 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:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (n + 1))) → X (↑i : ℕ)) (β := (i : ↥(Ioc a (n + 1))) → X (↑i : ℕ))
    (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.ProductMeasure
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)
⊢ 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:
fun_prop