awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)
i : ↥(Ioc a (a + 1))
refl :
  Eq (α := 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 : ℕ)))
      ((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)
      (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 : ℕ)))
      ((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

Tactic:
cases Nat.mem_Ioc_succ' i

Premises used: Nat.mem_Ioc_succ'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)
⊢ Eq (α := 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 : ℕ)))
      ((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)
      (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) ⋯))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
simp_rw :
  Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑{ toFun := fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦ cast ⋯ x,
          invFun := fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯),
          left_inv := ⋯, right_inv := ⋯ } :
      (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
⊢ Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑{ toFun := fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦ Eq.rec (motive := fun (x : ℕ) (h : a + 1 = x) ↦ X x) x ⋯,
          invFun := fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯),
          left_inv := ⋯, right_inv := ⋯ } :
      (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))

Tactic:
simp_rw [eqRec_eq_cast]

Premises used: eqRec_eq_cast
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑{ toFun := fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦ cast ⋯ x,
          invFun := fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯),
          left_inv := ⋯, right_inv := ⋯ } :
      (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))

Tactic:
measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)

Premises used: MeasurableEquiv.cast, measurable_pi_lambda, Iff.mp, MeasurableEquiv.measurable, eqRec_eq_cast._proof_1, Eq.symm, Nat.mem_Ioc_succ, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
refine :
  ∀ (i : ↥(Ioc a (a + 1))),
    HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β := MeasurableSpace (X (↑i : ℕ))) (inst (↑i : ℕ))
⊢ Measurable.{u_1, u_1} (α := X (a + 1)) (β := (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
    (⇑{ toFun := fun (x : X (a + 1)) (i : ↥(Ioc a (a + 1))) ↦ cast ⋯ x,
          invFun := fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
            x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯),
          left_inv := ⋯, right_inv := ⋯ } :
      (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))

Tactic:
refine measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)

Premises used: MeasurableEquiv.cast, measurable_pi_lambda, MeasurableEquiv.measurable
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
i : ↥(Ioc a (a + 1))
refl :
  HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β :=
    MeasurableSpace (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) : ℕ)))
    (inst (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) : ℕ))
⊢ HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β := MeasurableSpace (X (↑i : ℕ))) (inst (↑i : ℕ))

Tactic:
cases Nat.mem_Ioc_succ' i

Premises used: Nat.mem_Ioc_succ'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β :=
    MeasurableSpace (X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) : ℕ)))
    (inst (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) ⋯) : ℕ))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ι))
h :
  ∀ (x : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))),
    x ∈ IocProdIoc (X := X) a b c ⁻¹' Set.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ι)) Set.univ s ↔
      x ∈
        SProd.sprod (α := Set ((i : ↥(Ioc a b)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc b c)) → X (↑i : ι)))
          (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))
          (Set.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))
⊢ IocProdIoc (X := X) a b c ⁻¹' Set.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ι)) Set.univ s =
    SProd.sprod (α := Set ((i : ↥(Ioc a b)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc b c)) → X (↑i : ι)))
      (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))
      (Set.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))

Tactic:
ext x
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ι))
x : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))
h :
  (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ c),
      Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a c) a_1 ⋯))
        (IocProdIoc (X := X) a b c x (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a c) a_1 ⋯))) ↔
    (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))) ∧
      ∀ (a_1 : ι) (hp : b < a_1) (hq : a_1 ≤ c),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a : ι) ↦ a ∈ Ioc b c) a_1 ⋯))
⊢ x ∈ IocProdIoc (X := X) a b c ⁻¹' Set.pi (α := fun (i : ↥(Ioc a c)) ↦ X (↑i : ι)) Set.univ s ↔
    x ∈
      SProd.sprod (α := Set ((i : ↥(Ioc a b)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc b c)) → X (↑i : ι)))
        (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))
        (Set.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) ⋯ s))

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ι))
x : ((i : ↥(Ioc a b)) → X (↑i : ι)) × ((i : ↥(Ioc b c)) → X (↑i : ι))
⊢ (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ c),
      Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a c) a_1 ⋯))
        (IocProdIoc (X := X) a b c x (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a c) a_1 ⋯))) ↔
    (∀ (a_1 : ι) (hp : a < a_1) (hq : a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))) ∧
      ∀ (a_1 : ι) (hp : b < a_1) (hq : a_1 ≤ c),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a : ι) ↦ a ∈ Ioc b c) a_1 ⋯))

Tactic:
grind [IocProdIoc]

Premises used: 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 : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
h :
  ∀ (x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))),
    Membership.mem (γ := Set (((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
        (IicProdIoc (X := X) a b ⁻¹' Set.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ι)) Set.univ s) x ↔
      x ∈
        SProd.sprod (α := Set ((i : ↥(Iic a)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc a b)) → X (↑i : ι)))
          (Set.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ι)) Set.univ (frestrictLe₂ (π := fun (n : ι) ↦ Set (X n)) hab s))
          (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ
              (restrict₂ (π := fun (n : ι) ↦ Set (X n)) (s := Ioc a b) ⋯ s) :
            Set ((i : ↥(Ioc a b)) → X (↑i : ι)))
⊢ IicProdIoc (X := X) a b ⁻¹' Set.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ι)) Set.univ s =
    SProd.sprod (α := Set ((i : ↥(Iic a)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc a b)) → X (↑i : ι)))
      (Set.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ι)) Set.univ (frestrictLe₂ (π := fun (n : ι) ↦ Set (X n)) hab s))
      (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ
          (restrict₂ (π := fun (n : ι) ↦ Set (X n)) (s := Ioc a b) ⋯ s) :
        Set ((i : ↥(Ioc a b)) → X (↑i : ι)))

Tactic:
ext x
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ b),
      Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
        (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))) ↔
    (∀ (a_1 : ι) (b_1 : a_1 ≤ a),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 ⋯))) ∧
      ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))
⊢ Membership.mem (γ := Set (((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))))
      (IicProdIoc (X := X) a b ⁻¹' Set.pi (α := fun (i : ↥(Iic b)) ↦ X (↑i : ι)) Set.univ s) x ↔
    x ∈
      SProd.sprod (α := Set ((i : ↥(Iic a)) → X (↑i : ι))) (β := Set ((i : ↥(Ioc a b)) → X (↑i : ι)))
        (Set.pi (α := fun (i : ↥(Iic a)) ↦ X (↑i : ι)) Set.univ (frestrictLe₂ (π := fun (n : ι) ↦ Set (X n)) hab s))
        (Set.pi (α := fun (i : ↥(Ioc a b)) ↦ X (↑i : ι)) Set.univ
            (restrict₂ (π := fun (n : ι) ↦ Set (X n)) (s := Ioc a b) ⋯ s) :
          Set ((i : ↥(Ioc a b)) → X (↑i : ι)))

Tactic:
simp only [Set.mem_preimage, Set.mem_pi, Set.mem_univ, IicProdIoc_def, forall_const,
    Subtype.forall, mem_Iic, Set.mem_prod, frestrictLe₂_apply, restrict₂, mem_Ioc]

Premises used: Finset.mem_Iic, Subtype.forall, Set.mem_pi, IicProdIoc_def, Preorder.frestrictLe₂_apply, Set.mem_prod, Set.mem_univ, Finset.restrict₂, forall_const, Finset.mem_Ioc, Set.mem_preimage
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
⊢ (∀ (a_1 : ι) (b_1 : a_1 ≤ b),
      Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
        (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))) ↔
    (∀ (a_1 : ι) (b_1 : a_1 ≤ a),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 ⋯))) ∧
      ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
        Membership.mem (γ := Set (X a_1))
          (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
            Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
          (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))

Tactic:
⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩

Premises used: not_le, Iff.mpr, _private.0.IicProdIoc_preimage._simp_8, _private.0.IicProdIoc_preimage._simp_6, Finset.Ioc_subset_Iic_self, Finset.mem_Iic, Membership.mem, LE.le, Prod.fst, dite, Subtype.mk, _private.0.IicProdIoc_preimage.match_8, _private.0.IicProdIoc_preimage.match_9, And.intro, Iff.intro, Eq.substr, Iff.mp, Eq.mpr_not, Eq.refl, Finset.mem_Ioc, Finset.restrict₂._proof_1, Eq.mpr_prop, Prod.snd, 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 : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
hi : i ≤ a
⊢ Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
    (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:
h i (hi.trans hab)

Premises used: LE.le.trans
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
hi : i ≤ a
h₁ :
  x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i ⋯) =
    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 ⋯)
⊢ Membership.mem (γ := Set (X i))
    (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : ι)))
    (x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i ⋯))

Tactic:
convert! h i (hi.trans hab)

Premises used: LE.le.trans
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
hi : i ≤ a
h₁ h₂ : x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i ⋯) = x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯)
⊢ x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i ⋯) =
    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:
rw [dif_pos hi]

Premises used: dif_pos
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
h_1 : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
⊢ Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
    (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:
h i hi2
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
h_1 : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
h₁ :
  x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i ⋯) =
    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 ⋯)
⊢ Membership.mem (γ := Set (X i))
    (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i ⋯) : ι)))
    (x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i ⋯))

Tactic:
convert! h i hi2
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ b),
    Membership.mem (γ := Set (X a_1)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) a_1 ⋯))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 ⋯)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 ⋯))
i : ι
h_1 : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
h₁ h₂ :
  x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i ⋯) = x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) i ⋯)
⊢ x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i ⋯) =
    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:
rw [dif_neg (not_le.2 hi1)]

Premises used: not_le, Iff.mpr, dif_neg
-- 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
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a),
      Membership.mem (γ := Set (X a_1))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
        (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 ⋯))) ∧
    ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
      Membership.mem (γ := Set (X a_1))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
        (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))
i : ι
hi : i ≤ b
h1 :
  ∀ (a_1 : ι) (b_1 : a_1 ≤ a),
    Membership.mem (γ := Set (X a_1))
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
      (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 ⋯))
h2 :
  ∀ (a_1 : ι) (b_1 : a < a_1 ∧ a_1 ≤ b),
    Membership.mem (γ := Set (X a_1))
      (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) :
        Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 ⋯) : ι)))
      (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 ⋯))
pos :
  ∀ (hi3 : i ≤ a),
    Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
      (x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i ⋯))
neg :
  ∀ (hi3 : ¬i ≤ a),
    Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
      (x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) i ⋯))
⊢ Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i ⋯))
    (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:
split_ifs with hi3