awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 : ι) ⋯)
              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 (α := ((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 : ι))

Tactic:
refine measurable_pi_lambda _ (fun x ↦ ?_)

Premises used: measurable_pi_lambda
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 : ι) ⋯)
              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

Tactic:
by_cases h : x ≤ a
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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)
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

Tactic:
simpa [h] using measurable_fst.eval

Premises used: Measurable.eval, measurable_fst
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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)
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

Tactic:
simpa [h] using measurable_snd.eval

Premises used: measurable_snd, Measurable.eval
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
⊢ Eq (α := (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
    (⇑(IicProdIoc (X := X) hab) :
      (a : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
    (_root_.IicProdIoc (X := X) a b)

Tactic:
rfl

Premises used: dite, IicProdIoc, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
⊢ Eq (α := (a_1 : (i : ↥(Iic b)) → X (↑i : ι)) → ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι)))
    (⇑(symm (IicProdIoc (X := X) hab)) :
      (a_1 : (i : ↥(Iic b)) → X (↑i : ι)) → ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι)))
    fun (x : (i : ↥(Iic b)) → X (↑i : ι)) ↦ (frestrictLe₂ (π := X) hab x, restrict₂ (π := X) ⋯ x)

Tactic:
rfl

Premises used: Preorder.frestrictLe₂, Finset.restrict₂, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 ⋯)
                  else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯) :
                  X i))
              x)).2
        i =
      x.2 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

Tactic:
ext i
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))
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

Tactic:
simp [mem_Iic.1 i.2]

Premises used: Finset.mem_Iic, Iff.mp, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))
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 ⋯)
                else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯) :
                X i))
            x)).2
      i =
    x.2 i

Tactic:
simp [not_le.2 <| Set.mem_Ioi.1 i.2]

Premises used: not_le, Iff.mpr, Set.mem_Ioi, Iff.mp, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : (n : ι) → X n
⊢ (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))
      ((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 : ι))))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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)

Tactic:
measurable_pi_lambda _ (fun i ↦ ?_)

Premises used: measurable_pi_lambda
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι
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 ⋯)
              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 (α := ((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)

Tactic:
refine measurable_pi_lambda _ (fun i ↦ ?_)

Premises used: measurable_pi_lambda
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 ⋯)
              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

Tactic:
by_cases hi : i ≤ a
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 ⋯)
⊢ 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

Tactic:
simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]

Premises used: reduceDIte, Equiv.coe_fn_mk
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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
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 ⋯)
⊢ 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

Tactic:
simp only [Equiv.coe_fn_mk, hi, ↓reduceDIte]

Premises used: reduceDIte, Equiv.coe_fn_mk
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))) ↦
    c.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)

Tactic:
measurable_fst.eval

Premises used: Measurable.eval, measurable_fst
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))) ↦
    c.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)

Tactic:
exact measurable_fst.eval

Premises used: Measurable.eval, measurable_fst
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))) ↦
    c.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯)

Tactic:
measurable_snd.eval

Premises used: measurable_snd, Measurable.eval
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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 : ι))) ↦
    c.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Set.Ioi a) i ⋯)

Tactic:
exact measurable_snd.eval

Premises used: measurable_snd, Measurable.eval
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
x : X (a + 1)
⊢ (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) ⋯) : ℕ)))
      ((fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦
          (Eq.rec (motive := fun (x : ℕ) (h : a + 1 = x) ↦ X x) x ⋯ : X (↑i : ℕ)))
        x) =
    x

Tactic:
simp