awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
rw rw₁ :
  ∫⁻ (a : α), (((κ : (a : α) → Measure α) a : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
    ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π
⊢ (((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s =
    ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π

Tactic:
rw [Measure.bind_apply hs (Kernel.aemeasurable _)]

Premises used: MeasureTheory.Measure.bind_apply, ProbabilityTheory.Kernel.aemeasurable
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) s ∂π =
    ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π

Tactic:
simpa [restrict_univ] using (h_rev hs .univ).symm

Premises used: Eq.symm, ProbabilityTheory.Kernel.restrict_univ, MeasurableSet.univ
-- Module: Mathlib.Probability.Kernel.Invariance
Goal:
α : Type u_1
mα : MeasurableSpace α
κ : Kernel α α
inst : IsMarkovKernel κ
π : Measure α
h_rev : κ.IsReversible π
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π =
    (π : (a : Set α) → ℝ≥0∞) s

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.Invariance
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 ∂π
s₃ :
  ∫⁻ (x : α) in s, (((κ : (a : α) → Measure α) x : Measure α) : (a : Set α) → ℝ≥0∞) Set.univ ∂π =
    (π : (a : Set α) → ℝ≥0∞) s
⊢ Eq (α := ℝ≥0∞) ((((⇑κ : (a : α) → Measure α) ∘ₘ π : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((π : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

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

Premises used: MeasureTheory.Measure.bind, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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)

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 : (i : ι) → MeasurableSpace (X i)
a b c : ι
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
⊢ Measurable (α := ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))) (IocProdIoc (X := X) a b c)

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 : (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
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
⊢ 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
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
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)
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:
simpa [IocProdIoc, h] using measurable_fst.eval

Premises used: Measurable.eval, IocProdIoc, 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 : (i : ι) → MeasurableSpace (X i)
a b c : ι
i : ↥(Ioc a c)
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:
simpa [IocProdIoc, h] using measurable_snd.eval

Premises used: measurable_snd, Measurable.eval, IocProdIoc
-- 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 ι
a b : ι
⊢ Eq (α := (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) → (i : ↥(Iic b)) → X (↑i : ι))
    (IicProdIoc (X := X) a 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 : ι) ⋯)

Tactic:
rfl

Premises used: 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 ι
a b : ι
hab : a ≤ b
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
⊢ 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

Tactic:
ext x 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 ι
a b : ι
hab : a ≤ b
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:
simp [IicProdIoc, mem_Iic.1 i.2]

Premises used: Finset.mem_Iic, IicProdIoc, 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 ι
a b : ι
h :
  ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))) (i : ↥(Ioc a b)),
    (restrict₂ (π := X) ⋯ ∘ IicProdIoc (X := X) a b) x i = x.2 i
⊢ 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

Tactic:
ext x 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 ι
a b : ι
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
i : ↥(Ioc a b)
⊢ (restrict₂ (π := X) ⋯ ∘ IicProdIoc (X := X) a b) x i = x.2 i

Tactic:
simp [IicProdIoc, not_le.2 (mem_Ioc.1 i.2).1]

Premises used: not_le, Iff.mpr, And.left, IicProdIoc, Iff.mp, Finset.mem_Ioc, 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 ι
a : ι
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
⊢ 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

Tactic:
ext x 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 ι
a : ι
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:
simp [IicProdIoc, mem_Iic.1 i.2]

Premises used: Finset.mem_Iic, IicProdIoc, 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 ι
a b : ι
hba : b ≤ a
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
⊢ 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)

Tactic:
ext x 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 ι
a b : ι
hba : b ≤ a
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:
simp [IicProdIoc, (mem_Iic.1 i.2).trans hba]

Premises used: Finset.mem_Iic, IicProdIoc, Iff.mp, LE.le.trans, 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)
m n : ι
⊢ Measurable (α := ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) (IicProdIoc (X := X) m 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)
m n : ι
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
⊢ Measurable (α := ((i : ↥(Iic m)) → X (↑i : ι)) × ((i : ↥(Ioc m n)) → X (↑i : ι))) (IicProdIoc (X := X) m 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)
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
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
⊢ 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
-- 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)
m n : ι
i : ↥(Iic n)
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:
simpa [IicProdIoc, h] using measurable_fst.eval

Premises used: IicProdIoc, 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)
m n : ι
i : ↥(Iic n)
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:
simpa [IicProdIoc, h] using measurable_snd.eval

Premises used: IicProdIoc, 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
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
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 : ι) ⋯), 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)).2
        i =
      x.2 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

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 b : ι
hab : a ≤ b
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
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

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 b : ι
hab : a ≤ b
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
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 : ι) ⋯), 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)).2
      i =
    x.2 i

Tactic:
simp [not_le.2 (mem_Ioc.1 i.2).1]

Premises used: not_le, Iff.mpr, And.left, Iff.mp, Finset.mem_Ioc, 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 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
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 : ι) ⋯)
            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

Tactic:
by_cases hi : i.1 ≤ a

Premises used: Subtype.val
-- 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 : (i : ↥(Iic b)) → X (↑i : ι)
i : ↥(Iic b)
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

Tactic:
simp [hi]
-- 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 : (i : ↥(Iic b)) → X (↑i : ι)
i : ↥(Iic b)
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

Tactic:
simp [hi]
-- 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
⊢ 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:
measurable_pi_lambda _ (fun x ↦ ?_)

Premises used: measurable_pi_lambda