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 ι
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 ⋯))
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 ⋯))

Tactic:
h1 i hi3

Premises used: Set.Mem
-- 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 ⋯))
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 ⋯))

Tactic:
exact h1 i hi3
-- 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 ⋯))
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 ⋯))

Tactic:
h2 i ⟨not_le.1 hi3, hi⟩

Premises used: not_le, Set.Mem, And.intro, Iff.mp
-- 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 ⋯))
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 ⋯))

Tactic:
exact h2 i ⟨not_le.1 hi3, hi⟩

Premises used: not_le, And.intro, Iff.mp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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) ⋯)
rw₁ rw₂ :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) hba) ⋯) (deterministic (frestrictLe₂ (π := X) hba) ⋯)
⊢ partialTraj (X := X) κ a b = deterministic (frestrictLe₂ (π := X) hba) ⋯

Tactic:
rw [partialTraj, dif_pos hba]

Premises used: dif_pos, ProbabilityTheory.Kernel.partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a : ℕ
rw :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯) ⋯) Kernel.id
⊢ partialTraj (X := X) κ a a = Kernel.id

Tactic:
rw [partialTraj_le le_rfl]

Premises used: le_rfl, ProbabilityTheory.Kernel.partialTraj_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a : ℕ
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯) ⋯) Kernel.id

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
rw rw₁ :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic 0)) → X (↑i : ℕ)))
    (deterministic (frestrictLe₂ (π := X) ⋯) ⋯) (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic 0)) → X (↑i : ℕ))) (partialTraj (X := X) κ a 0)
    (deterministic (frestrictLe₂ (π := X) ⋯) ⋯)

Tactic:
rw [partialTraj_le zero_le]

Premises used: zero_le, ProbabilityTheory.Kernel.partialTraj_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
inl :
  ∀ (hab : a ≤ a),
    partialTraj (X := X) κ a a =
      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 :
              (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
                k x) ↦
          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)))
        hab
inr :
  ∀ (hab_1 : a < b),
    partialTraj (X := X) κ a b =
      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 :
              (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ)))
                k x) ↦
          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)))
        hab
⊢ partialTraj (X := X) κ a b =
    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 :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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)))
      hab

Tactic:
obtain rfl | hab := eq_or_lt_of_le hab

Premises used: eq_or_lt_of_le, rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ a
⊢ partialTraj (X := X) κ a a =
    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 :
            (fun (b : ℕ) (x : a ≤ b) ↦ Kernel.{u_1, u_1} ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))) k
              x) ↦
        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)))
      hab

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
⊢ ¬b + 1 ≤ a

Tactic:
lia
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
hab : a ≤ b
rw :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
    (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)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
          partialTraj (X := X) κ a b)
        (_root_.IicProdIoc (X := X) b (b + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ)))
⊢ Eq (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (b + 1))) → X (↑i : ℕ))) (partialTraj (X := X) κ a (b + 1))
    (map (β := ((i : ↥(Iic b)) → X (↑i : ℕ)) × ((i : ↥(Ioc b (b + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
      (Kernel.id ×ₖ (κ b).map (⇑(piSingleton (X := X) b) : (a : X (b + 1)) → (i : ↥(Ioc b (b + 1))) → X (↑i : ℕ)) ∘ₖ
        partialTraj (X := X) κ a b)
      (_root_.IicProdIoc (X := X) b (b + 1)))

Tactic:
rw [partialTraj, dif_neg (by lia)]

Premises used: dif_neg, ProbabilityTheory.Kernel.partialTraj
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
    (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)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic a)) → X (↑i : ℕ)) × ((i : ↥(Ioc a (a + 1))) → X (↑i : ℕ))) (mβ := Prod.instMeasurableSpace)
        (Kernel.id ×ₖ (κ a).map (⇑(piSingleton (X := X) a) : (a_1 : X (a + 1)) → (i : ↥(Ioc a (a + 1))) → X (↑i : ℕ)) ∘ₖ
          partialTraj (X := X) κ a a)
        (_root_.IicProdIoc (X := X) a (a + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (a + 1))) → X (↑i : ℕ)))

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (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)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → 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 : ℕ)) ∘ₖ
          partialTraj (X := X) κ a k)
        (_root_.IicProdIoc (X := X) k (k + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
succ : a ≤ k + 1
⊢ Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))
    (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)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))
    (map (β := ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)) × ((i : ↥(Ioc (k + 1) (k + 1 + 1))) → X (↑i : ℕ))) (mβ :=
        Prod.instMeasurableSpace)
        (Kernel.id ×ₖ
            map (κ (k + 1))
              (⇑(piSingleton (X := X) (k + 1)) : (a : X (k + 1 + 1)) → (i : ↥(Ioc (k + 1) (k + 1 + 1))) → X (↑i : ℕ)) ∘ₖ
          partialTraj (X := X) κ a (k + 1))
        (_root_.IicProdIoc (X := X) (k + 1) (k + 1 + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1 + 1))) → X (↑i : ℕ)))

Tactic:
rw [Nat.leRec_succ, ← partialTraj_le_def]

Premises used: ProbabilityTheory.Kernel.partialTraj_le_def, Nat.leRec_succ
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
k : ℕ
hak : a ≤ k
hk :
  Eq.{u_1 + 1} (α := Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
    (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)))
        ⋯ :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → 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 : ℕ)) ∘ₖ
          partialTraj (X := X) κ a k)
        (_root_.IicProdIoc (X := X) k (k + 1)) :
      Kernel ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic (k + 1))) → X (↑i : ℕ)))
⊢ a ≤ k + 1

Tactic:
lia
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
inl : ∀ (hab : a ≤ b), IsSFiniteKernel (partialTraj (X := X) κ a b)
inr : ∀ (hba : b ≤ a), IsSFiniteKernel (partialTraj (X := X) κ a b)
⊢ IsSFiniteKernel (partialTraj (X := X) κ a b)

Tactic:
obtain hab | hba := le_total a b

Premises used: le_total
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
inl :
  IsSFiniteKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) Kernel.id
⊢ IsSFiniteKernel (partialTraj (X := X) κ a a)

Tactic:
rw [partialTraj_self]

Premises used: ProbabilityTheory.Kernel.partialTraj_self
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b : ℕ
⊢ IsSFiniteKernel.{u_1, u_1} (α := (i : ↥(Iic a)) → X (↑i : ℕ)) (mα :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic a)) ↦ X (↑i : ℕ))) Kernel.id

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b k : ℕ
hak : a ≤ k
h : IsSFiniteKernel (partialTraj (X := X) κ a k)
inl :
  IsSFiniteKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic (k + 1))) ↦ 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 : ℕ)) ∘ₖ
        partialTraj (X := X) κ a k)
      (_root_.IicProdIoc (X := X) k (k + 1)))
⊢ IsSFiniteKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (partialTraj (X := X) κ a (k + 1))

Tactic:
rw [partialTraj_succ_of_le hak]

Premises used: ProbabilityTheory.Kernel.partialTraj_succ_of_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a_1 b_1 c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
a b k : ℕ
hak : a ≤ k
h : IsSFiniteKernel (partialTraj (X := X) κ a k)
⊢ IsSFiniteKernel (β := (i : ↥(Iic (k + 1))) → X (↑i : ℕ)) (mβ :=
    MeasurableSpace.pi (X := fun (i : ↥(Iic (k + 1))) ↦ 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 : ℕ)) ∘ₖ
        partialTraj (X := X) κ a k)
      (_root_.IicProdIoc (X := X) k (k + 1)))

Tactic:
infer_instance