awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
⊢ ∃ (z : X (k + 1)),
    ∀ (x : (i : ℕ) → X i) (n : ℕ),
      ε ≤
        lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
          (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) z)
have obtain : ∀ (x : X (k + 1)) (hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)),
  ∃ (z : X (k + 1)),
    ∀ (x : (i : ℕ) → X i) (n : ℕ),
      ε ≤
        lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
          (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) z)
Tactic: obtain ⟨x, hx⟩ : ∃ x, ε ≤ l (update (updateFinset x_ _ y) (k + 1) x) := by
    have : ∫⁻ x, l (update (updateFinset x_ _ y) (k + 1) x) ∂(κ k y) ≠ ∞ :=
      ne_top_of_le_ne_top fin_bound <| lintegral_le_const <| ae_of_all _
        fun y ↦ le_of_tendsto' (tendstoF _) <| fun _ ↦ F_le _ _
    obtain ⟨x, hx⟩ := exists_lintegral_le this
    refine ⟨x, (ε_le_lint x_).trans ?_⟩
    rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]
    exact ENNReal.measurable_of_tendsto (by fun_prop) (tendsto_pi_nhds.2 htendsto)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
⊢ ∃ (z : X (k + 1)),
    ∀ (x : (i : ℕ) → X i) (n : ℕ),
      ε ≤
        lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
          (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) z)
have refine : ∀ (x' : (i : ℕ) → X i) (n : ℕ),
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x)
Tactic: refine ⟨x, fun x' n ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
⊢ ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x)
have this : ε ≤ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
Tactic: have := le_trans hx ((anti _).le_of_tendsto (tendstoF _) n)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
⊢ ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x)
have h : lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x) =
  lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
⊢ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x) =
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
have h : ∀ (i : ℕ) (hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)),
  update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x i =
    update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x i
Tactic: refine (hcte n).dependsOn_lmarginalPartialTraj _ (mf n) fun i hi ↦ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)
⊢ update (β := X) (updateFinset (π := X) x' (Iic k) y) (k + 1) x i =
    update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x i
have h : Eq.{u_1 + 1} (α := X i)
  (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x sorry
  else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i sorry) else x' i)
  (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x sorry
  else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i sorry) else x_ i)
Tactic: simp only [update, updateFinset, mem_Iic]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x' i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x_ i)
have pos : ∀ (h1 : i = k + 1),
  Eq.{u_1 + 1} (α := X i) (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x sorry : X i)
    (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x sorry : X i)
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)
pos :
  ∀ (h1 : i = k + 1),
    Eq.{u_1 + 1} (α := X i) (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯ : X i)
      (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯ : X i)
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x' i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x_ i)
have pos₁ : ∀ (h1 : ¬i = k + 1) (h2 : i ≤ k),
  Eq (α := X i)
    (y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i sorry) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i sorry) : ℕ))
    (y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i sorry))
Tactic: split_ifs with h1 h2
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst_1 : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (α := X) (f n) (↑(Iic (a n)) : Set ℕ)
mf : ∀ (n : ℕ), Measurable (f n)
bound : ℝ≥0∞
fin_bound : bound ≠ ∞
le_bound : ∀ (n : ℕ) (x : (n : ℕ) → X n), f n x ≤ bound
k : ℕ
anti : ∀ (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto :
  ∀ (x : (n : ℕ) → X n), Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X (↑i : ℕ)
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (f n) (updateFinset (π := X) x (Iic k) y)
h : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
F : (n : ℕ) → ((n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))
f_eq :
  ∀ (x : (n : ℕ) → X n) (n : ℕ),
    lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (f n) x) atTop
      (𝓝 (lmarginalPartialTraj (X := X) κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj (X := X) κ k (k + 1) l (updateFinset (π := X) x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this :
  ε ≤
    lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n) (update (β := X) (updateFinset (π := X) x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ (↑(Iic (k + 1)) : Set ℕ)
pos :
  ∀ (h1 : i = k + 1),
    Eq.{u_1 + 1} (α := X i) (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯ : X i)
      (Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯ : X i)
pos₁ :
  ∀ (h1 : ¬i = k + 1) (h2 : i ≤ k),
    Eq (α := X i)
      (y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) : ℕ))
      (y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯))
⊢ Eq.{u_1 + 1} (α := X i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x' i)
    (if h : i = k + 1 then Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x) x ⋯
    else if h : i ≤ k then y (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic k) i ⋯) else x_ i)
have neg : ∀ (h1 : ¬i = k + 1) (h2 : ¬i ≤ k), x' i = x_ i
Tactic: split_ifs with h1 h2