awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
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))) ↦ 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 : ℕ))
have 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 sorry x,
        invFun := fun (x : (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ↦
          x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry),
        left_inv := sorry, right_inv := sorry } :
    (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))
Tactic: simp_rw [eqRec_eq_cast]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
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 : ℕ))
have refine : ∀ (i : ↥(Ioc a (a + 1))),
  HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β := MeasurableSpace (X (↑i : ℕ))) (inst (↑i : ℕ))
Tactic: refine measurable_pi_lambda _ (fun i ↦ (MeasurableEquiv.cast _ ?_).measurable)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
i : ↥(Ioc a (a + 1))
⊢ HEq.{u_1 + 1} (α := MeasurableSpace (X (a + 1))) (inst (a + 1)) (β := MeasurableSpace (X (↑i : ℕ))) (inst (↑i : ℕ))
have 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) sorry) : ℕ)))
  (inst (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Ioc a (a + 1)) (a + 1) sorry) : ℕ))
Tactic: cases Nat.mem_Ioc_succ' i
Cleared hypotheses: 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
a b c : ι
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X (↑i : ι))
⊢ 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))
have 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)) sorry s))
        (Set.pi (α := fun (i : ↥(Ioc b c)) ↦ X (↑i : ι)) Set.univ (restrict₂ (π := fun (n : ι) ↦ Set (X n)) sorry s))
Tactic: ext 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
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 : ι))
⊢ 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))
have 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 sorry))
      (IocProdIoc (X := X) a b c x (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a c) a_1 sorry))) ↔
  (∀ (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 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 sorry) : ι)))
        (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 sorry))) ∧
    ∀ (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 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a c) a_1 sorry) : ι)))
        (x.2 (Subtype.mk (p := fun (a : ι) ↦ a ∈ Ioc b c) a_1 sorry))
Tactic: simp
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (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 : ι)))
have 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) sorry s) :
          Set ((i : ↥(Ioc a b)) → X (↑i : ι)))
Tactic: ext 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 ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
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 : ι)))
have 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 sorry))
      (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 sorry)
      else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 sorry))) ↔
  (∀ (a_1 : ι) (b_1 : a_1 ≤ a),
      Membership.mem (γ := Set (X a_1))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
        (x.1 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Iic a) a_1 sorry))) ∧
    ∀ (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 sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) a_1 sorry) : ι)))
        (x.2 (Subtype.mk (p := fun (a_2 : ι) ↦ a_2 ∈ Ioc a b) a_1 sorry))
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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 ⋯))
have h : ∀
  (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 sorry))
        (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 sorry)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 sorry)))
  (i : ι) (hi : i ≤ a),
  Membership.mem (γ := Set (X i))
    (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i sorry) : Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i sorry) : ι)))
    (x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i sorry))
Tactic: refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X (↑i : ι))
x : ((i : ↥(Iic a)) → X (↑i : ι)) × ((i : ↥(Ioc a b)) → X (↑i : ι))
h :
  ∀
    (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 (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 ⋯))
⊢ (∀ (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 ⋯))
have h₁ : ∀
  (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 sorry))
        (if h : a_1 ≤ a then x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) a_1 sorry)
        else x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) a_1 sorry)))
  (i : ι),
  a < i ∧ i ≤ b →
    ∀ (hi1 : a < i) (hi2 : i ≤ b),
      Membership.mem (γ := Set (X i))
        (s (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i sorry) :
          Set (X (↑(Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic b) i sorry) : ι)))
        (x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i sorry))
Tactic: refine ⟨fun h ↦ ⟨fun i hi ↦ ?_, fun i ⟨hi1, hi2⟩ ↦ ?_⟩, fun ⟨h1, h2⟩ i hi ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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 (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 ⋯))
have h₁ : x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i sorry) =
  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)
Tactic: convert! h i (hi.trans hab)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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
⊢ 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 ⋯)
have h₁ : x.1 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Iic a) i sorry) = x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry)
Tactic: rw [dif_pos hi]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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 (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 ⋯))
have h₁ : x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i sorry) =
  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)
Tactic: convert! h i hi2
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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
⊢ 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 ⋯)
have h₁ : x.2 (Subtype.mk (p := fun (a_1 : ι) ↦ a_1 ∈ Ioc a b) i sorry) = x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) i sorry)
Tactic: rw [dif_neg (not_le.2 hi1)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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 ⋯))
⊢ 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 ⋯))
have pos : ∀ (hi3 : i ≤ a),
  Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i sorry))
    (x.1 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Iic a) i sorry))
Tactic: split_ifs with hi3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Maps (goal)
Goal:
ι : Type u_1
inst : LinearOrder ι
inst_1 : LocallyFiniteOrder ι
inst_2 : DecidableLE ι
X : ι → Type u_2
inst_3 : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
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 ⋯))
⊢ 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 ⋯))
have neg : ∀ (hi3 : ¬i ≤ a),
  Membership.mem (γ := Set (X i)) (s (Subtype.mk (p := fun (a : ι) ↦ a ∈ Iic b) i sorry))
    (x.2 (Subtype.mk (p := fun (x : ι) ↦ x ∈ Ioc a b) i sorry))
Tactic: split_ifs with hi3
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hba : b ≤ a
⊢ partialTraj (X := X) κ a b = deterministic (frestrictLe₂ (π := X) hba) ⋯
have rw : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (if h : b ≤ a then deterministic (frestrictLe₂ (π := X) h) sorry
  else
    Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
      Kernel.id
      (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → X (↑i : ℕ))) ↦
        map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ :=
          Prod.instMeasurableSpace)
          (Kernel.id ×ₖ (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) ∘ₖ
            κ_k)
          (_root_.IicProdIoc (X := X) k (k + 1)))
      sorry)
  (deterministic (frestrictLe₂ (π := X) hba) sorry)
Tactic: rw [partialTraj, dif_pos hba]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hba : b ≤ a
rw :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (if h : b ≤ a then deterministic (frestrictLe₂ (π := X) h) ⋯
    else
      Nat.leRec (motive := fun (b : ℕ) (x : a ≤ b) ↦ Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
        Kernel.id
        (fun (k : ℕ) (x : a ≤ k) (κ_k : Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic k)) → X (↑i : ℕ))) ↦
          map (β := ((i : ↥(Iic k)) → X (↑i : ℕ)) × ((i : ↥(Ioc k (k + 1))) → X (↑i : ℕ))) (mβ :=
            Prod.instMeasurableSpace)
            (Kernel.id ×ₖ
                (κ k).map (⇑(piSingleton (X := X) k) : (a : X (k + 1)) → (i : ↥(Ioc k (k + 1))) → X (↑i : ℕ)) ∘ₖ
              κ_k)
            (_root_.IicProdIoc (X := X) k (k + 1)))
        ⋯)
    (deterministic (frestrictLe₂ (π := X) hba) ⋯)
⊢ partialTraj (X := X) κ a b = deterministic (frestrictLe₂ (π := X) hba) ⋯
have rw₁ : Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
  (deterministic (frestrictLe₂ (π := X) hba) sorry) (deterministic (frestrictLe₂ (π := X) hba) sorry)
Tactic: rw [partialTraj, dif_pos hba]