awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
e_f : ∀ (x : (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)) (i : ↥(Iic n)), restrict₂ (π := X) ⋯ x i = cast ⋯ x i
⊢ Eq (α := Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) (Measure.map (restrict₂ (π := X) ⋯) (μ ((Iic n).sup id)))
    (Measure.map (α := (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)) (cast ⋯) (μ ((Iic n).sup id)))

Tactic:
congr with x i
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
x : (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)
i : ↥(Iic n)
rw rw₁ : (↑(Iic n) : Set ℕ) = (↑(Iic n) : Set ℕ)
⊢ (↑(Iic ((Iic n).sup id)) : Set ℕ) = (↑(Iic n) : Set ℕ)

Tactic:
rw [sup_Iic n]

Premises used: Finset.sup_Iic
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
x : (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)
i : ↥(Iic n)
e_f : x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) ⋯) = cast ⋯ x i
e_f₁ e_f₂ :
  Eq (α := X (↑i : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) ⋯) :
      X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) ⋯) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ (↑(Iic ((Iic n).sup id)) : Set ℕ)) (↑i : ℕ) ⋯))
⊢ restrict₂ (π := X) ⋯ x i = cast ⋯ x i

Tactic:
rw [restrict₂, cast_pi (by rw [sup_Iic n])]

Premises used: _private.0.cast_pi, Finset.restrict₂
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ (π := X) hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
⊢ J.sup id ≤ I.sup id

Tactic:
have sls : J.sup id ≤ I.sup id := sup_mono hJI
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ (π := X) hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (J.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
hf : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
hg₁ : Measurable.{u_1, u_1} (α := (i : ↥I) → X (↑i : ℕ)) (restrict₂ (π := X) hJI)
hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)
⊢ Eq (α := Measure ((j : ↥J) → X (↑j : ℕ))) (Measure.map (restrict₂ (π := X) ⋯) (μ (J.sup id)))
    (Measure.map (restrict₂ (π := X) hJI) (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id))))

Tactic:
rw [Measure.map_map, restrict₂_comp_restrict₂,
    ← restrict₂_comp_restrict₂ J.subset_Iic_sup_id (Iic_subset_Iic.2 sls), ← Measure.map_map,
    ← frestrictLe₂.eq_def sls, h (J.sup id) (I.sup id) sls]

Premises used: Iff.mpr, id, Preorder.frestrictLe₂.eq_def, Finset.Iic_subset_Iic, Finset.sup, Finset.subset_Iic_sup_id, MeasureTheory.Measure.map_map, Finset.restrict₂_comp_restrict₂
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ (π := X) hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (J.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ (π := X) hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) ⋯)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
h : ∀ (a b : ℕ) (hab : a ≤ b), Measure.map (frestrictLe₂ (π := X) hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable.{u_1, u_1} (α := (i : ↥I) → X (↑i : ℕ)) (restrict₂ (π := X) hJI)

Tactic:
fun_prop
-- 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 : ℕ
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ IsProjectiveMeasureFamily (α := X)
    (inducedFamily (X := X) fun (b : ℕ) ↦
      (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀)

Tactic:
isProjectiveMeasureFamily_inducedFamily _
    (fun _ _ ↦ partialTraj_map_frestrictLe₂_apply (κ := κ) x₀)

Premises used: MeasureTheory.isProjectiveMeasureFamily_inducedFamily, ProbabilityTheory.Kernel.partialTraj_map_frestrictLe₂_apply
-- 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 b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
rw :
  Eq (α := ℝ≥0∞)
    ((projectiveFamilyContent (α := X) ⋯ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₁ :
  Eq (α := ℝ≥0∞)
    (((inducedFamily (X := X)
              (fun (b : ℕ) ↦
                (partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
                  x₀)
              (Iic b) :
            Measure ((k : ↥(Iic b)) → X (↑k : ℕ))) :
          (a : Set ((j : ↥(Iic b)) → X (↑j : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((j : ↥(Iic b)) → X (↑j : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((trajContent (X := X) κ x₀ : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) (cylinder (α := X) (Iic b) S) : ℝ≥0∞)
    ((((partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) x₀ :
            Measure ((i : ↥(Iic b)) → X (↑i : ℕ))) :
          (a : Set ((i : ↥(Iic b)) → X (↑i : ℕ))) → ℝ≥0∞)
        S :
      ℝ≥0∞)

Tactic:
rw [trajContent, projectiveFamilyContent_cylinder _ mS, inducedFamily_Iic]

Premises used: MeasureTheory.projectiveFamilyContent_cylinder, MeasureTheory.inducedFamily_Iic, ProbabilityTheory.Kernel.trajContent
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
rw :
  ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      S.indicator 1
        a ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (cylinder (α := X) (Iic b) S).indicator 1
        (updateFinset (π := X) x₀ (Iic b)
          z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)
⊢ (trajContent (X := X) κ (frestrictLe (π := X) a x₀) : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞)
      (cylinder (α := X) (Iic b) S) =
    lmarginalPartialTraj (X := X) κ a b ((cylinder (α := X) (Iic b) S).indicator 1) x₀

Tactic:
rw [trajContent_cylinder mS, ← lintegral_indicator_one mS, lmarginalPartialTraj]

Premises used: ProbabilityTheory.Kernel.trajContent_cylinder, MeasureTheory.lintegral_indicator_one, ProbabilityTheory.Kernel.lmarginalPartialTraj
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
e_f :
  ∀ (x : (i : ↥(Iic b)) → X (↑i : ℕ)),
    Eq (α := ℝ≥0∞) (S.indicator 1 x) ((cylinder (α := X) (Iic b) S).indicator 1 (updateFinset (π := X) x₀ (Iic b) x))
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X (↑i : ℕ)),
      S.indicator 1
        a ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀) =
    ∫⁻ (z : (i : ↥(Iic b)) → X (↑i : ℕ)),
      (cylinder (α := X) (Iic b) S).indicator 1
        (updateFinset (π := X) x₀ (Iic b)
          z) ∂(partialTraj (X := X) κ a b : (a : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Iic b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x₀)

Tactic:
congr with x
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
e_f : x ∈ S ↔ updateFinset (π := X) x₀ (Iic b) x ∈ cylinder (α := X) (Iic b) S
⊢ Eq (α := ℝ≥0∞) (S.indicator 1 x) ((cylinder (α := X) (Iic b) S).indicator 1 (updateFinset (π := X) x₀ (Iic b) x))

Tactic:
apply Set.indicator_const_eq_indicator_const

Premises used: Set.indicator_const_eq_indicator_const
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
e_f : x ∈ S ↔ (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) ∈ S
⊢ x ∈ S ↔ updateFinset (π := X) x₀ (Iic b) x ∈ cylinder (α := X) (Iic b) S

Tactic:
rw [mem_cylinder]

Premises used: MeasureTheory.mem_cylinder
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
e_f : ∀ (i : ↥(Iic b)), x i = (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) i
⊢ x ∈ S ↔ (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) ∈ S

Tactic:
congrm (fun i ↦ ?_) ∈ S
-- 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)
b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (n : ℕ) → X n
a : ℕ
x : (i : ↥(Iic b)) → X (↑i : ℕ)
i : ↥(Iic b)
⊢ x i = (Iic b).restrict (π := X) (updateFinset (π := X) x₀ (Iic b) x) i

Tactic:
simp [updateFinset, i.2]

Premises used: Function.updateFinset, Subtype.property
-- 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 : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
s : Set ((n : ℕ) → X n)
⊢ Ne (α := ℝ≥0∞) ((trajContent (X := X) κ x : (a : Set ((i : ℕ) → X i)) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
projectiveFamilyContent_ne_top (isProjectiveMeasureFamily_partialTraj κ x)

Premises used: ProbabilityTheory.Kernel.isProjectiveMeasureFamily_partialTraj, MeasureTheory.projectiveFamilyContent_ne_top
-- 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)
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)
⊢ Nonempty.{u_1 + 1} (X 0)

Tactic:
⟨y ⟨0, mem_Iic.2 zero_le⟩⟩

Premises used: Iff.mpr, zero_le, Finset.mem_Iic, Nonempty.intro, Subtype.mk, OfNat.ofNat
-- 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)
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)
⊢ Nonempty.{u_1 + 1} (X 0)

Tactic:
exact ⟨y ⟨0, mem_Iic.2 zero_le⟩⟩
-- 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)
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)
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)
⊢ Nonempty.{u_1 + 1} ((i : ↥(Iic m)) → X (↑i : ℕ))

Tactic:
have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
-- 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)
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)
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)
this : Nonempty.{u_1 + 1} ((i : ↥(Iic m)) → X (↑i : ℕ))
⊢ Nonempty.{u_1 + 1} (X (m + 1))

Tactic:
nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

Premises used: MeasureTheory.nonempty_of_isProbabilityMeasure, Classical.ofNonempty, DFunLike.coe
-- 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)
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)
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)
this : Nonempty.{u_1 + 1} ((i : ↥(Iic m)) → X (↑i : ℕ))
⊢ Nonempty.{u_1 + 1} (X (m + 1))

Tactic:
exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

Premises used: MeasureTheory.nonempty_of_isProbabilityMeasure, Classical.ofNonempty, DFunLike.coe
-- 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)
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)
n : ℕ
hz : Nonempty.{u_1 + 1} (X 0)
hi : ∀ (m : ℕ) (hm : ∀ m_1 ≤ m, Nonempty.{u_1 + 1} (X m_1)), Nonempty.{u_1 + 1} (X (m + 1))
⊢ Nonempty.{u_1 + 1} (X n)

Tactic:
induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨y ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

Premises used: Nat.case_strong_induction_on
-- 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)
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)
⊢ ∀ (n : ℕ), Nonempty.{u_1 + 1} (X n)

Tactic:
have _ n : Nonempty (X n) := by
    induction n using Nat.case_strong_induction_on with
    | hz => exact ⟨y ⟨0, mem_Iic.2 zero_le⟩⟩
    | hi m hm =>
      have : Nonempty (Π i : Iic m, X i) :=
        ⟨fun i ↦ @Classical.ofNonempty _ (hm i.1 (mem_Iic.1 i.2))⟩
      exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)
-- 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)
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)
⊢ ∀ (x : (n : ℕ) → X n), Tendsto (fun (x_1 : ℕ) ↦ F x_1 x) atTop (𝓝 (l x))

Tactic:
have tendstoF x : Tendsto (F · x) atTop (𝓝 (l x)) := htendsto x
-- 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)
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))
x : (n : ℕ) → X n
n : ℕ
simp_rw :
  lmarginalPartialTraj (X := X) κ k (a n) (f n) x =
    lmarginalPartialTraj (X := X) κ k (k + 1) (lmarginalPartialTraj (X := X) κ (k + 1) (a n) (f n)) x
⊢ lmarginalPartialTraj (X := X) κ k (a n) (f n) x = lmarginalPartialTraj (X := X) κ k (k + 1) (F n) x

Tactic:
simp_rw [F]