awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((piecewise (s := s) hs κ η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
have simp_rw : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ mβ (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
  (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
  else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
Tactic: simp_rw [piecewise_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
have pos : a ∈ s →
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
pos :
  a ∈ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ ((κ : (a : α) → Measure β) a) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
have neg : a ∉ s →
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ ((η : (a : α) → Measure β) a) fun (b : β) ↦ g b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ (Measure.restrict ((piecewise (s := s) hs κ η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
have simp_rw : Eq.{u_3 + 1} (α := E)
  (@integral _ _ _ _ mβ
    (Measure.restrict (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
  (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
  else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
Tactic: simp_rw [piecewise_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ
      (Measure.restrict (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) t) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
have pos : a ∈ s →
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Integral (goal)
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
η : Kernel α β
s : Set α
hs : MeasurableSet s
inst_2 : DecidablePred fun (x : α) ↦ x ∈ s
a : α
g : β → E
t : Set β
pos :
  a ∈ s →
    Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
      (@integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ mβ
      (Measure.restrict (if a ∈ s then (κ : (a : α) → Measure β) a else (η : (a : α) → Measure β) a) t) fun (b : β) ↦
      g b)
    (if a ∈ s then @integral _ _ _ _ mβ (Measure.restrict ((κ : (a : α) → Measure β) a) t) fun (b : β) ↦ g b
    else @integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
have neg : a ∉ s →
  Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
    (@integral _ _ _ _ mβ (Measure.restrict ((η : (a : α) → Measure β) a) t) fun (b : β) ↦ g b)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
⊢ Eq (α := Kernel α α) (κ ∘ₖ const α μ) (const α μ)
have rw : Eq (α := Kernel α α) (const α ((⇑κ : (a : α) → Measure α) ∘ₘ μ)) (const α μ)
Tactic: rw [comp_const κ μ, hκ.def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
rw : Eq (α := Kernel α α) (const α ((⇑κ : (a : α) → Measure α) ∘ₘ μ)) (const α μ)
⊢ Eq (α := Kernel α α) (κ ∘ₖ const α μ) (const α μ)
have rw₁ : Eq (α := Kernel α α) (const α μ) (const α μ)
Tactic: rw [comp_const κ μ, hκ.def]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
⊢ (κ ∘ₖ η).Invariant μ
have inl : IsEmpty α → (κ ∘ₖ η).Invariant μ
Tactic: rcases isEmpty_or_nonempty α with _ | hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
inl : IsEmpty α → (κ ∘ₖ η).Invariant μ
⊢ (κ ∘ₖ η).Invariant μ
have inr : ∀ (hα : Nonempty α), (κ ∘ₖ η).Invariant μ
Tactic: rcases isEmpty_or_nonempty α with _ | hα
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
⊢ (κ ∘ₖ η).Invariant μ
have inr : (⇑(κ ∘ₖ η) : (a : α) → Measure α) ∘ₘ μ = μ
Tactic: rw [Invariant, ← Measure.comp_assoc, hη, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
inr : (⇑(κ ∘ₖ η) : (a : α) → Measure α) ∘ₘ μ = μ
⊢ (κ ∘ₖ η).Invariant μ
have inr₁ : Measure.bind (α := α) (mα := mα) ((⇑η : (a : α) → Measure α) ∘ₘ μ) (⇑κ : (a : α) → Measure α) = μ
Tactic: rw [Invariant, ← Measure.comp_assoc, hη, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
inr : (⇑(κ ∘ₖ η) : (a : α) → Measure α) ∘ₘ μ = μ
inr₁ : Measure.bind (α := α) (mα := mα) ((⇑η : (a : α) → Measure α) ∘ₘ μ) (⇑κ : (a : α) → Measure α) = μ
⊢ (κ ∘ₖ η).Invariant μ
have inr₂ : (⇑κ : (a : α) → Measure α) ∘ₘ μ = μ
Tactic: rw [Invariant, ← Measure.comp_assoc, hη, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ η : Kernel α α
μ : Measure α
hκ : κ.Invariant μ
hη : η.Invariant μ
hα : Nonempty α
inr : (⇑(κ ∘ₖ η) : (a : α) → Measure α) ∘ₘ μ = μ
inr₁ : Measure.bind (α := α) (mα := mα) ((⇑η : (a : α) → Measure α) ∘ₘ μ) (⇑κ : (a : α) → Measure α) = μ
inr₂ : (⇑κ : (a : α) → Measure α) ∘ₘ μ = μ
⊢ (κ ∘ₖ η).Invariant μ
have inr₃ : μ = μ
Tactic: rw [Invariant, ← Measure.comp_assoc, hη, hκ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
⊢ κ.Invariant π
have h : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ (((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
have rw : ∫⁻ (a : α), (((κ : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
  ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
Tactic: rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have s₁ : (((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s =
  ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
Tactic: calc
    (κ ∘ₘ π) s = ∫⁻ x, κ x s ∂π := by rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
             _ = ∫⁻ x in s, κ x Set.univ ∂π := by simpa [restrict_univ] using (h_rev hs .univ).symm
             _ = π s := by simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
s₁ :
  (((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have s₂ : ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
  ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π
Tactic: calc
    (κ ∘ₘ π) s = ∫⁻ x, κ x s ∂π := by rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
             _ = ∫⁻ x in s, κ x Set.univ ∂π := by simpa [restrict_univ] using (h_rev hs .univ).symm
             _ = π s := by simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.Invariance (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
s₁ :
  (((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
s₂ :
  ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
    ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have s₃ : ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π =
  (π : (a : Set α) → ℝ≥0∞) s
Tactic: calc
    (κ ∘ₘ π) s = ∫⁻ x, κ x s ∂π := by rw [Measure.bind_apply hs (Kernel.aemeasurable _)]
             _ = ∫⁻ x in s, κ x Set.univ ∂π := by simpa [restrict_univ] using (h_rev hs .univ).symm
             _ = π s := by simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : (i : ι) → MeasurableSpace (X i)
a b c : ι
⊢ Measurable (α := ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) (IocProdIoc (X := X) a b c)
have refine : ∀ (i : ↥(Ioc a c)),
  Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
    IocProdIoc (X := X) a b c c_1 i
Tactic: refine measurable_pi_lambda _ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
⊢ Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
    IocProdIoc (X := X) a b c c_1 i
have pos : ∀ (h : (↑i : ι) ≤ b),
  Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
    IocProdIoc (X := X) a b c c_1 i
Tactic: by_cases h : i ≤ b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
pos :
  ∀ (h : (↑i : ι) ≤ b),
    Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
      IocProdIoc (X := X) a b c c_1 i
⊢ Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
    IocProdIoc (X := X) a b c c_1 i
have neg : ∀ (h : ¬(↑i : ι) ≤ b),
  Measurable (β := X (↑i : ι)) fun (c_1 : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) ↦
    IocProdIoc (X := X) a b c c_1 i
Tactic: by_cases h : i ≤ b
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
⊢ Eq (α := ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι)) → (i : ↥(Iic a)) → X (↑i : ι))
    (frestrictLe₂ (π := X) hab ∘ IicProdIoc (X := X) a b) Prod.fst
have h : ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic a)),
  (frestrictLe₂ (π := X) hab ∘ IicProdIoc (X := X) a b) x i = x.1 i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
⊢ Eq (α := ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι)) → (i : ↥(Ioc a b)) → X (↑i : ι))
    (restrict₂ (π := X) ⋯ ∘ IicProdIoc (X := X) a b) Prod.snd
have h : ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Ioc a b)),
  (restrict₂ (π := X) sorry ∘ IicProdIoc (X := X) a b) x i = x.2 i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a : ι
⊢ Eq (α := (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a a)) → X (↑i : ι))) → (i : ↥(Iic a)) → X (↑i : ι))
    (IicProdIoc (X := X) a a) Prod.fst
have h : ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a a)) → X (↑i : ι))) (i : ↥(Iic a)),
  IicProdIoc (X := X) a a x i = x.1 i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hba : b ≤ a
⊢ Eq (α := (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
    (IicProdIoc (X := X) a b) (frestrictLe₂ (π := X) hba ∘ Prod.fst)
have h : ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)),
  IicProdIoc (X := X) a b x i = (frestrictLe₂ (π := X) hba ∘ Prod.fst) x i
Tactic: ext x i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
inst_4 : (i : ι) → MeasurableSpace (X i)
m n : ι
⊢ Measurable (α := ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) (IicProdIoc (X := X) m n)
have refine : ∀ (i : ↥(Iic n)),
  Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
    IicProdIoc (X := X) m n c i
Tactic: refine measurable_pi_lambda _ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
inst_4 : (i : ι) → MeasurableSpace (X i)
m n : ι
i : ↥(Iic n)
⊢ Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
    IicProdIoc (X := X) m n c i
have pos : ∀ (h : (↑i : ι) ≤ m),
  Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
    IicProdIoc (X := X) m n c i
Tactic: by_cases h : i ≤ m
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
inst_4 : (i : ι) → MeasurableSpace (X i)
m n : ι
i : ↥(Iic n)
pos :
  ∀ (h : (↑i : ι) ≤ m),
    Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
      IicProdIoc (X := X) m n c i
⊢ Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
    IicProdIoc (X := X) m n c i
have neg : ∀ (h : ¬(↑i : ι) ≤ m),
  Measurable (β := X (↑i : ι)) fun (c : ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) ↦
    IicProdIoc (X := X) m n c i
Tactic: by_cases h : i ≤ m
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
inst_4 : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
⊢ (fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦
        ((fun (i : ↥(Iic a)) ↦ x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯), fun (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯)) :
          ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
      ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)) ↦
          (if h : (↑i : ι) ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) (↑i : ι) ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) (↑i : ι) ⋯) :
            X (↑i : ι)))
        x) =
    x
have fst : ∀ (i : ↥(Iic a)),
  ((fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦
            ((fun (i : ↥(Iic a)) ↦ x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) sorry), fun (i : ↥(Ioc a b)) ↦
                x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) sorry)) :
              ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
          ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)) ↦
              (if h : (↑i : ι) ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) (↑i : ι) sorry)
                else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) (↑i : ι) sorry) :
                X (↑i : ι)))
            x)).1
      i =
    x.1 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
inst_4 : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
fst :
  ∀ (i : ↥(Iic a)),
    ((fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦
              ((fun (i : ↥(Iic a)) ↦ x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯), fun (i : ↥(Ioc a b)) ↦
                  x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯)) :
                ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
            ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)) ↦
                (if h : (↑i : ι) ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) (↑i : ι) ⋯)
                  else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) (↑i : ι) ⋯) :
                  X (↑i : ι)))
              x)).1
        i =
      x.1 i
⊢ (fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦
        ((fun (i : ↥(Iic a)) ↦ x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯), fun (i : ↥(Ioc a b)) ↦
            x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) ⋯)) :
          ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
      ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)) ↦
          (if h : (↑i : ι) ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) (↑i : ι) ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) (↑i : ι) ⋯) :
            X (↑i : ι)))
        x) =
    x
have snd : ∀ (i : ↥(Ioc a b)),
  ((fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦
            ((fun (i : ↥(Iic a)) ↦ x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) sorry), fun (i : ↥(Ioc a b)) ↦
                x (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) (↑i : ι) sorry)) :
              ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
          ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Iic b)) ↦
              (if h : (↑i : ι) ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) (↑i : ι) sorry)
                else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) (↑i : ι) sorry) :
                X (↑i : ι)))
            x)).2
      i =
    x.2 i
Tactic: ext i