-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : Eq.{u_1 + 1} (α := Set ((n : ℕ) → X n)) (⋂ (n : ℕ), A n) ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X (↑i : ℕ)
h_1 : ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)
a : (n : ℕ) → ℕ
S : (n : ℕ) → Set ((i : ↥(Iic (a n))) → X (↑i : ℕ))
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (α := X) (Iic (a n)) (S n)
χ : (n : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞ := fun (n : ℕ) ↦ (A n).indicator 1
mχ : ∀ (n : ℕ), Measurable (χ n)
χ_dep : ∀ (n : ℕ), DependsOn (α := X) (χ n) (↑(Iic (a n)) : Set ℕ)
lma_const :
  ∀ (x y : (i : ℕ) → X i) (n : ℕ),
    lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀) =
      lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) y (Iic p) x₀)
χ_anti : Antitone χ
lma_inv :
  ∀ (k M n : ℕ) (h : a n ≤ M), lmarginalPartialTraj (X := X) κ k M (χ n) = lmarginalPartialTraj (X := X) κ k (a n) (χ n)
anti_lma :
  ∀ (k : ℕ) (x : (n : ℕ) → X n), Antitone (β := ℝ≥0∞) fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x
l : (k : ℕ) → (x : (n : ℕ) → X n) → ℝ≥0∞
hl :
  ∀ (k : ℕ) (x : (n : ℕ) → X n),
    Tendsto (fun (n : ℕ) ↦ lmarginalPartialTraj (X := X) κ k (a n) (χ n) x) atTop (𝓝 (l k x))
l_const : ∀ (x y : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = l p (updateFinset (π := X) y (Iic p) x₀)
ε : ℝ≥0∞
hε : ∀ (x : (i : ℕ) → X i), l p (updateFinset (π := X) x (Iic p) x₀) = ε
hpos :
  ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj (X := X) κ p (a n) (χ n) (updateFinset (π := X) x (Iic p) x₀)
χ_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), χ n x ≤ 1
ind : (k : ℕ) → (y : (i : ↥(Iic k)) → X (↑i : ℕ)) → X (k + 1)
hind :
  ∀ (k : ℕ) (y : (i : ↥(Iic k)) → X (↑i : ℕ))
    (h :
      ∀ (x : (i : ℕ) → X i) (n : ℕ),
        ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) y))
    (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤
      lmarginalPartialTraj (X := X) κ (k + 1) (a n) (χ n)
        (update (β := X) (updateFinset (π := X) x (Iic k) y) (k + 1) (ind k y))
z : (n : ℕ) → X n := iterateInduction (X := X) x₀ ind
k_1 k : ℕ
hn : p ≤ k
h :
  ∀ (x : (i : ℕ) → X i) (n : ℕ),
    ε ≤ lmarginalPartialTraj (X := X) κ k (a n) (χ n) (updateFinset (π := X) x (Iic k) (frestrictLe (π := X) k z))
x : (i : ℕ) → X i
n i : ℕ
h₁ :
  (if i ≤ k + 1 then iterateInduction (X := X) x₀ ind i else x i) =
    if h : i = k + 1 then
      Eq.rec (motive := fun (x : ℕ) (x_1 : k + 1 = x) ↦ X x)
        (ind k fun (i : ↥(Iic k)) ↦ iterateInduction (X := X) x₀ ind (↑i : ℕ)) ⋯
    else if i ≤ k then iterateInduction (X := X) x₀ ind i else x i
⊢ updateFinset (π := X) x (Iic (k + 1)) (frestrictLe (π := X) (k + 1) z) i =
    update (β := X) (updateFinset (π := X) x (Iic k) fun (i : ↥(Iic k)) ↦ z (↑i : ℕ)) (k + 1)
      (ind k fun (i : ↥(Iic k)) ↦ z (↑i : ℕ)) i

Tactic:
simp only [updateFinset, mem_Iic, frestrictLe_apply, dite_eq_ite, update, z]

Premises used: Function.update, Function.updateFinset, Finset.mem_Iic, Preorder.frestrictLe_apply, dite_eq_ite