awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 b)) → X (↑i : ι)
i : ↥(Iic b)
⊢ (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 : ι)))
      ((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 : ι))))
        x)
      i =
    x i
have pos : ∀ (hi : (↑i : ι) ≤ a),
  (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 : ι)))
      ((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 : ι))))
        x)
      i =
    x i
Tactic: by_cases hi : i.1 ≤ a
-- 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 b)) → X (↑i : ι)
i : ↥(Iic b)
pos :
  ∀ (hi : (↑i : ι) ≤ a),
    (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 : ι)))
        ((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 : ι))))
          x)
        i =
      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 : ι)))
      ((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 : ι))))
        x)
      i =
    x i
have neg : ∀ (hi : ¬(↑i : ι) ≤ a),
  (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 : ι)))
      ((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 : ι))))
        x)
      i =
    x i
Tactic: by_cases hi : i.1 ≤ a
-- 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
⊢ Measurable (α := ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (β := (i : ↥(Iic b)) → X (↑i : ι))
    (⇑{
          toFun := 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 : ι) ⋯),
          invFun := 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 : ι) ⋯)),
          left_inv := ⋯, right_inv := ⋯ } :
      (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
have refine : ∀ (x : ↥(Iic b)),
  Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
    ({
          toFun := 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),
          invFun := 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)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
      c x
Tactic: refine measurable_pi_lambda _ (fun x ↦ ?_)
-- 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 : ↥(Iic b)
⊢ Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
    ({
          toFun := 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 : ι) ⋯),
          invFun := 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 : ι) ⋯)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
      c x
have pos : ∀ (h : (↑x : ι) ≤ a),
  Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
    ({
          toFun := 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),
          invFun := 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)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
      c x
Tactic: by_cases h : x ≤ a
-- 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 : ↥(Iic b)
pos :
  ∀ (h : (↑x : ι) ≤ a),
    Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
      ({
            toFun := 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 : ι) ⋯),
            invFun := 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 : ι) ⋯)),
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
        c x
⊢ Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
    ({
          toFun := 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 : ι) ⋯),
          invFun := 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 : ι) ⋯)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
      c x
have neg : ∀ (h : ¬(↑x : ι) ≤ a),
  Measurable (β := X (↑x : ι)) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) ↦
    ({
          toFun := 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),
          invFun := 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)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
      c x
Tactic: by_cases h : x ≤ a
-- 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 : ι
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))
⊢ (fun (x : (n : ι) → X n) ↦
        ((fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)) :
          ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))))
      ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
          (if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯) :
            X i))
        x) =
    x
have fst : ∀ (i : ↥(Iic a)),
  ((fun (x : (n : ι) → X n) ↦
            ((fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)) :
              ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))))
          ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
              (if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
                else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) 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 : ι
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))
fst :
  ∀ (i : ↥(Iic a)),
    ((fun (x : (n : ι) → X n) ↦
              ((fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)) :
                ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))))
            ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
                (if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
                  else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯) :
                  X i))
              x)).1
        i =
      x.1 i
⊢ (fun (x : (n : ι) → X n) ↦
        ((fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)) :
          ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))))
      ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
          (if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯) :
            X i))
        x) =
    x
have snd : ∀ (i : (↑(Set.Ioi a) : Type u_1)),
  ((fun (x : (n : ι) → X n) ↦
            ((fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)) :
              ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))))
          ((fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
              (if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
                else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i sorry) :
                X i))
            x)).2
      i =
    x.2 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 : ι
⊢ Measurable (α := ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (β := (n : ι) → X n)
    (⇑{
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := ⋯, right_inv := ⋯ } :
      (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
have refine : ∀ (i : ι),
  Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i sorry),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X 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)
a i : ι
⊢ Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
have pos : ∀ (hi : i ≤ a),
  Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i sorry),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
Tactic: by_cases hi : i ≤ a
-- 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 i : ι
pos :
  ∀ (hi : i ≤ a),
    Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
      ({
            toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
              if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
              else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
            invFun := fun (x : (n : ι) → X n) ↦
              (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
            left_inv := ⋯, right_inv := ⋯ } :
          (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
        c i
⊢ Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
have neg : ∀ (hi : ¬i ≤ a),
  Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i sorry),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := sorry, right_inv := sorry } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
Tactic: by_cases hi : i ≤ a
-- 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 i : ι
hi : i ≤ a
⊢ Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
have pos : Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
  c.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
Tactic: simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]
-- 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 i : ι
hi : ¬i ≤ a
⊢ Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
    ({
          toFun := fun (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) (i : ι) ↦
            if hi : i ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
            else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯),
          invFun := fun (x : (n : ι) → X n) ↦
            (fun (i : ↥(Iic a)) ↦ x (↑i : ι), fun (i : (↑(Set.Ioi a) : Type u_1)) ↦ x (↑i : ι)),
          left_inv := ⋯, right_inv := ⋯ } :
        (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) → (n : ι) → X n)
      c i
have neg : Measurable (β := X i) fun (c : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : (↑(Set.Ioi a) : Type u_1)) → X (↑i : ι))) ↦
  c.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i sorry)
Tactic: simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)
i : ↥(Ioc a (a + 1))
⊢ (fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦ (Eq.rec (motive := fun (x : ℕ) (h : a + 1 = x) ↦ X x) x ⋯ : X (↑i : ℕ)))
      ((fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
          (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) :
            X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) : ℕ)))
        x)
      i =
    x i
have refl : Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry) : ℕ))
  ((fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦
      (Eq.rec (motive := fun (x : ℕ) (h : a + 1 = x) ↦ X x) x sorry : X (↑i : ℕ)))
    ((fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
        (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry) :
          X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry) : ℕ)))
      x)
    (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry))
Tactic: cases Nat.mem_Ioc_succ' i
Cleared hypotheses: i