awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
inl : ∀ (hba : b ≤ a), lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
have inr : ∀ (hab : a ≤ b), lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
Tactic: obtain hba | hab := le_total b a
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hba : b ≤ a
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
have inl : f x = f y
Tactic: rw [Kernel.lmarginalPartialTraj_le κ hba mf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hab : a ≤ b
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y
have inr : ∫⁻ (x_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
    f
      (Function.updateFinset (π := X) x (Ioc a b)
        x_1) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a x) =
  ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
    f
      (Function.updateFinset (π := X) y (Ioc a b)
        x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) sorry) :
        (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
      (frestrictLe (π := X) a y)
Tactic: rw [lmarginalPartialTraj_eq_lintegral_map mf, lmarginalPartialTraj_eq_lintegral_map mf]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hab : a ≤ b
⊢ ∫⁻ (x_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc a b)
          x_1) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) y (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a y)
have inr : ∀ (i : ↥(Iic a)), frestrictLe (π := X) a x i = frestrictLe (π := X) a y i
Tactic: congrm ∫⁻ z : _, ?_ ∂(partialTraj κ a b).map _ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hab : a ≤ b
inr : ∀ (i : ↥(Iic a)), frestrictLe (π := X) a x i = frestrictLe (π := X) a y i
⊢ ∫⁻ (x_1 : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) x (Ioc a b)
          x_1) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a x) =
    ∫⁻ (x : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
      f
        (Function.updateFinset (π := X) y (Ioc a b)
          x) ∂((partialTraj (X := X) κ a b).map (restrict₂ (π := X) ⋯) :
          (a_1 : (i : ↥(Iic a)) → X (↑i : ℕ)) → Measure ((i : ↥(Ioc a b)) → X (↑i : ℕ)))
        (frestrictLe (π := X) a y)
have inr₁ : ∀ (z : (i : ↥(Ioc a b)) → X (↑i : ℕ)),
  f (Function.updateFinset (π := X) x (Ioc a b) z) = f (Function.updateFinset (π := X) y (Ioc a b) z)
Tactic: congrm ∫⁻ z : _, ?_ ∂(partialTraj κ a b).map _ (fun i ↦ ?_)
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hab : a ≤ b
z : (i : ↥(Ioc a b)) → X (↑i : ℕ)
⊢ f (Function.updateFinset (π := X) x (Ioc a b) z) = f (Function.updateFinset (π := X) y (Ioc a b) z)
have inr : ∀ i ∈ (↑(Iic b) : Set ℕ) \ (↑(Ioc a b) : Set ℕ), x i = y i
Tactic: refine hf.updateFinset _ ?_
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj (goal)
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : DependsOn (α := X) f (↑(Iic b) : Set ℕ)
mf : Measurable f
x y : (i : ℕ) → X i
hxy : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
hab : a ≤ b
z : (i : ↥(Ioc a b)) → X (↑i : ℕ)
⊢ ∀ i ∈ (↑(Iic b) : Set ℕ) \ (↑(Ioc a b) : Set ℕ), x i = y i
have inr : ∀ i ∈ (↑(Iic b \ Ioc a b) : Set ℕ), x i = y i
Tactic: rwa [← coe_sdiff, Iic_diff_Ioc_self_of_le hab]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a b : ℕ
h : a = b
⊢ Eq.{u_1 + 2} (α := Type u_1) ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))
have refl : Eq.{u_1 + 2} (α := Type u_1) ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ))
Tactic: cases h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
s t : Set ℕ
h : s = t
x : (i : (↑s : Type)) → X (↑i : ℕ)
i : (↑t : Type)
⊢ Eq.{u_1 + 1} (α := X (↑i : ℕ)) (cast ⋯ x i : X (↑i : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) (↑i : ℕ) ⋯) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) (↑i : ℕ) ⋯) : ℕ))
have refl : ∀ (i : (↑s : Type)),
  Eq.{u_1 + 1} (α := X (↑i : ℕ)) (cast sorry x i : X (↑i : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) (↑i : ℕ) sorry) : X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ s) (↑i : ℕ) sorry) : ℕ))
Tactic: cases h
Cleared hypotheses: t, h, i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
⊢ Measure.map (cast ⋯) (μ a) = μ b
have refl : Measure.map (cast sorry) (μ a) = μ a
Tactic: cases h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
⊢ HEq.{u_1 + 1} (α := MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance (β :=
    MeasurableSpace ((i : ↥(Iic b)) → X (↑i : ℕ))) inferInstance
have refl : HEq.{u_1 + 1} (α := MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance (β :=
  MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance
Tactic: cases h
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
⊢ frestrictLe (π := X) a (iterateInduction (X := X) x ind) = x
have h : ∀ (i : ↥(Iic a)), frestrictLe (π := X) a (iterateInduction (X := X) x ind) i = x i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
i : ↥(Iic a)
⊢ frestrictLe (π := X) a (iterateInduction (X := X) x ind) i = x i
have h : iterateInduction (X := X) x ind (↑i : ℕ) = x i
Tactic: simp only [frestrictLe_apply]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
i : ↥(Iic a)
⊢ iterateInduction (X := X) x ind (↑i : ℕ) = x i
have h : ∀ (hj : 0 ∈ Iic a),
  Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
    (iterateInduction (X := X) x ind (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj))
Tactic: obtain ⟨(zero | j), hj⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
i : ↥(Iic a)
h :
  ∀ (hj : 0 ∈ Iic a),
    Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
      (iterateInduction (X := X) x ind (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
      (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj))
⊢ iterateInduction (X := X) x ind (↑i : ℕ) = x i
have h₁ : ∀ (j : ℕ) (hj : j + 1 ∈ Iic a),
  Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
    (iterateInduction (X := X) x ind (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
Tactic: obtain ⟨(zero | j), hj⟩ := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
hj : 0 ∈ Iic a
⊢ Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
    (iterateInduction (X := X) x ind (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj))
have h : Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ)) (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 sorry))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj))
Tactic: rw [iterateInduction]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
    (iterateInduction (X := X) x ind (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
have h : Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
  (if h : j + 1 ≤ a then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) sorry)
  else ind j fun (i : ↥(Iic j)) ↦ iterateInduction (X := X) x ind (↑i : ℕ))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
Tactic: rw [iterateInduction]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
j : ℕ
hj : j + 1 ∈ Iic a
⊢ Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
    (if h : j + 1 ≤ a then x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) ⋯)
    else ind j fun (i : ↥(Iic j)) ↦ iterateInduction (X := X) x ind (↑i : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
have h : Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj) : ℕ))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) sorry)) (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
Tactic: rw [dif_pos (mem_Iic.1 hj)]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
⊢ IsProjectiveLimit (α := X) ν μ ↔
    ∀ ⦃n : ℕ⦄,
      a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
have refine : ∀
  (h :
    ∀ ⦃n : ℕ⦄,
      a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n)))
  (I : Finset ℕ), Measure.map (I.restrict (π := X)) ν = μ I
Tactic: refine ⟨fun h n _ ↦ h (Iic n), fun h I ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h :
  ∀ ⦃n : ℕ⦄,
    a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
I : Finset ℕ
⊢ Measure.map (I.restrict (π := X)) ν = μ I
have this : I ⊆ Iic (max (I.sup id) a)
Tactic: have := (I.subset_Iic_sup_id.trans (Iic_subset_Iic.2 (le_max_left (I.sup id) a)))
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h :
  ∀ ⦃n : ℕ⦄,
    a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measure.map (I.restrict (π := X)) ν = μ I
have hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (max (I.sup id) a))) → X (↑i : ℕ)) (restrict₂ (π := X) this)
Tactic: rw [← restrict₂_comp_restrict this, ← Measure.map_map, ← frestrictLe, h (le_max_right _ _), ← hμ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h :
  ∀ ⦃n : ℕ⦄,
    a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (max (I.sup id) a))) → X (↑i : ℕ)) (restrict₂ (π := X) this)
⊢ Measure.map (I.restrict (π := X)) ν = μ I
have hf : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (max (I.sup id) a)).restrict (π := X))
Tactic: rw [← restrict₂_comp_restrict this, ← Measure.map_map, ← frestrictLe, h (le_max_right _ _), ← hμ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
⊢ IsProjectiveLimit (α := X) ν μ ↔
    ∀ (n : ℕ), Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
have rw : (∀ ⦃n : ℕ⦄,
    0 ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))) ↔
  ∀ (n : ℕ), Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))
Tactic: rw [isProjectiveLimit_nat_iff' hμ _ 0]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
⊢ inducedFamily (X := X) μ (Iic n) = μ n
have rw : Eq (α := Measure ((k : ↥(Iic n)) → X (↑k : ℕ))) (Measure.map (restrict₂ (π := X) sorry) (μ ((Iic n).sup id)))
  (Measure.map (α := (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)) (cast sorry) (μ ((Iic n).sup id)))
Tactic: rw [inducedFamily, ← measure_cast (sup_Iic n) μ]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
⊢ 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)))
have e_f : ∀ (x : (i : ↥(Iic ((Iic n).sup id))) → X (↑i : ℕ)) (i : ↥(Iic n)), restrict₂ (π := X) sorry x i = cast sorry x i
Tactic: congr with x i
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
⊢ (↑(Iic ((Iic n).sup id)) : Set ℕ) = (↑(Iic n) : Set ℕ)
have rw : (↑(Iic n) : Set ℕ) = (↑(Iic n) : Set ℕ)
Tactic: rw [sup_Iic n]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
⊢ restrict₂ (π := X) ⋯ x i = cast ⋯ x i
have e_f : x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) sorry) = cast sorry x i
Tactic: rw [restrict₂, cast_pi (by rw [sup_Iic n])]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
⊢ restrict₂ (π := X) ⋯ x i = cast ⋯ x i
have e_f₁ : Eq (α := X (↑i : ℕ))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) sorry) :
    X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic ((Iic n).sup id)) (↑i : ℕ) sorry) : ℕ))
  (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ (↑(Iic ((Iic n).sup id)) : Set ℕ)) (↑i : ℕ) sorry))
Tactic: rw [restrict₂, cast_pi (by rw [sup_Iic n])]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (hypothesis)
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
⊢ inducedFamily (X := X) μ J = Measure.map (restrict₂ (π := X) hJI) (inducedFamily (X := X) μ I)
have sls : J.sup id ≤ I.sup id
Tactic: have sls : J.sup id ≤ I.sup id := sup_mono hJI
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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
⊢ 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))))
have hg : Measurable.{u_1, u_1} (α := (i : ↥(Iic (J.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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) ⋯)
⊢ 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))))
have hf : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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) ⋯)
⊢ 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))))
have hg₁ : Measurable.{u_1, u_1} (α := (i : ↥I) → X (↑i : ℕ)) (restrict₂ (π := X) hJI)
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]
-- Lean 4 proof step from Mathlib.Probability.Kernel.IonescuTulcea.Traj (goal)
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)
⊢ 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))))
have hf₁ : Measurable.{u_1, u_1} (α := (i : ↥(Iic (I.sup id))) → X (↑i : ℕ)) (restrict₂ (π := X) sorry)
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]
-- 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)
a b : ℕ
S : Set ((i : ↥(Iic b)) → X (↑i : ℕ))
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X (↑i : ℕ)
⊢ 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∞)
have rw : Eq (α := ℝ≥0∞)
  ((projectiveFamilyContent (α := X) sorry : (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]