awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
Goal:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c_1 : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X (↑i : ℕ)) (X (n + 1))
inst : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn (α := X) f (↑(Iic a) : Set ℕ)
c d : ℕ
hac : a ≤ c
had : a ≤ d
hcd : c ≤ d
hcb : c ≤ b
inr : f = lmarginalPartialTraj (X := X) κ b d f
inr₁ inr₂ : f = f
⊢ lmarginalPartialTraj (X := X) κ b c f = lmarginalPartialTraj (X := X) κ b d f

Tactic:
rw [hf.lmarginalPartialTraj_of_le c mf (hac.trans hcb),
      hf.lmarginalPartialTraj_of_le d mf (hac.trans hcb)]

Premises used: DependsOn.lmarginalPartialTraj_of_le, LE.le.trans
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
inr : ∀ (hab : a ≤ b), 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

Tactic:
obtain hba | hab := le_total b a

Premises used: le_total
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
inl : f x = f y
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y

Tactic:
rw [Kernel.lmarginalPartialTraj_le κ hba mf]

Premises used: ProbabilityTheory.Kernel.lmarginalPartialTraj_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
⊢ f x = f y

Tactic:
hf fun i hi ↦ hxy i (Iic_subset_Iic.2 hba hi)

Premises used: Iff.mpr, Finset.Iic_subset_Iic
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
⊢ f x = f y

Tactic:
exact hf fun i hi ↦ hxy i (Iic_subset_Iic.2 hba hi)

Premises used: Iff.mpr, Finset.Iic_subset_Iic
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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 :
  ∫⁻ (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)
⊢ lmarginalPartialTraj (X := X) κ a b f x = lmarginalPartialTraj (X := X) κ a b f y

Tactic:
rw [lmarginalPartialTraj_eq_lintegral_map mf, lmarginalPartialTraj_eq_lintegral_map mf]

Premises used: ProbabilityTheory.Kernel.lmarginalPartialTraj_eq_lintegral_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
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)
⊢ ∫⁻ (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)

Tactic:
congrm ∫⁻ z : _, ?_ ∂(partialTraj κ a b).map _ (fun i ↦ ?_)

Premises used: ProbabilityTheory.Kernel.map, ProbabilityTheory.Kernel.partialTraj, DFunLike.coe
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
i : ↥(Iic a)
⊢ frestrictLe (π := X) a x i = frestrictLe (π := X) a y i

Tactic:
hxy i.1 i.2

Premises used: Finset.restrict, Preorder.frestrictLe, Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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
i : ↥(Iic a)
⊢ frestrictLe (π := X) a x i = frestrictLe (π := X) a y i

Tactic:
exact hxy i.1 i.2

Premises used: Subtype.val, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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)

Tactic:
hf.updateFinset _ ?_

Premises used: DependsOn.updateFinset
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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 : ℕ)
inr : ∀ i ∈ (↑(Iic b) : Set ℕ) \ (↑(Ioc a b) : Set ℕ), x i = y i
⊢ f (Function.updateFinset (π := X) x (Ioc a b) z) = f (Function.updateFinset (π := X) y (Ioc a b) z)

Tactic:
refine hf.updateFinset _ ?_

Premises used: DependsOn.updateFinset
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
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 : ℕ)
inr : ∀ i ∈ (↑(Iic b \ Ioc a b) : Set ℕ), x i = y i
inr₁ inr₂ inr₃ inr₄ : ∀ i ∈ (↑(Iic a) : Set ℕ), x i = y i
⊢ ∀ i ∈ (↑(Iic b) : Set ℕ) \ (↑(Ioc a b) : Set ℕ), x i = y i

Tactic:
rwa [← coe_sdiff, Iic_diff_Ioc_self_of_le hab]

Premises used: Finset.coe_sdiff, Finset.Iic_diff_Ioc_self_of_le
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
a b : ℕ
h : a = b
refl : Eq.{u_1 + 2} (α := Type u_1) ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ))
⊢ Eq.{u_1 + 2} (α := Type u_1) ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic b)) → X (↑i : ℕ))

Tactic:
cases h
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
a : ℕ
⊢ Eq.{u_1 + 2} (α := Type u_1) ((i : ↥(Iic a)) → X (↑i : ℕ)) ((i : ↥(Iic a)) → X (↑i : ℕ))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
s t : Set ℕ
h : s = t
x : (i : (↑s : Type)) → X (↑i : ℕ)
i : (↑t : Type)
refl :
  ∀ (i : (↑s : 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 : ℕ) ⋯) : ℕ))
⊢ 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 : ℕ) ⋯) : ℕ))

Tactic:
cases h
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
s : Set ℕ
x : (i : (↑s : Type)) → X (↑i : ℕ)
i : (↑s : 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 : ℕ) ⋯) : ℕ))

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
refl : Measure.map (cast ⋯) (μ a) = μ a
⊢ Measure.map (cast ⋯) (μ a) = μ b

Tactic:
cases h
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
⊢ Measure.map (cast ⋯) (μ a) = μ a

Tactic:
Measure.map_id

Premises used: MeasureTheory.Measure.map_id, cast
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
⊢ Measure.map (cast ⋯) (μ a) = μ a

Tactic:
exact Measure.map_id

Premises used: MeasureTheory.Measure.map_id
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
h : a = b
refl :
  HEq.{u_1 + 1} (α := MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance (β :=
    MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance
⊢ HEq.{u_1 + 1} (α := MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance (β :=
    MeasurableSpace ((i : ↥(Iic b)) → X (↑i : ℕ))) inferInstance

Tactic:
cases h
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ HEq.{u_1 + 1} (α := MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance (β :=
    MeasurableSpace ((i : ↥(Iic a)) → X (↑i : ℕ))) inferInstance

Tactic:
rfl
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
a k : ℕ
h : ¬k + 1 ≤ a
i : ↥(Iic k)
⊢ (↑i : ℕ) < k.succ

Tactic:
Nat.lt_succ_of_le (mem_Iic.1 i.2)

Premises used: Finset.mem_Iic, Nat.lt_succ_of_le, Iff.mp, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
a k : ℕ
h : ¬k + 1 ≤ a
i : ↥(Iic k)
⊢ (↑i : ℕ) < k.succ

Tactic:
exact Nat.lt_succ_of_le (mem_Iic.1 i.2)

Premises used: Finset.mem_Iic, Nat.lt_succ_of_le, Iff.mp, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
a k : ℕ
h : ¬k + 1 ≤ a
i : ↥(Iic k)
⊢ (↑i : ℕ) < k.succ

Tactic:
decreasing_by exact Nat.lt_succ_of_le (mem_Iic.1 i.2)

Premises used: Finset.mem_Iic, Nat.lt_succ_of_le, Iff.mp, Subtype.property
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
a : ℕ
x : (i : ↥(Iic a)) → X (↑i : ℕ)
ind : (n : ℕ) → ((i : ↥(Iic n)) → X (↑i : ℕ)) → X (n + 1)
h : ∀ (i : ↥(Iic a)), frestrictLe (π := X) a (iterateInduction (X := X) x ind) i = x i
⊢ frestrictLe (π := X) a (iterateInduction (X := X) x ind) = x

Tactic:
ext i
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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 : iterateInduction (X := X) x ind (↑i : ℕ) = x i
⊢ frestrictLe (π := X) a (iterateInduction (X := X) x ind) i = x i

Tactic:
simp only [frestrictLe_apply]

Premises used: Preorder.frestrictLe_apply
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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))
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))
⊢ iterateInduction (X := X) x ind (↑i : ℕ) = x i

Tactic:
obtain ⟨(zero | j), hj⟩ := i
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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
h h₁ :
  Eq (α := X (↑(Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj) : ℕ))
    (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 ⋯)) (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) 0 hj))
⊢ 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:
rw [iterateInduction]

Premises used: iterateInduction
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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
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) ⋯)
    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))
⊢ 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:
rw [iterateInduction]

Premises used: iterateInduction
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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
h 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) ⋯)) (x (Subtype.mk (p := fun (x : ℕ) ↦ x ∈ Iic a) (j + 1) hj))
⊢ 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))

Tactic:
rw [dif_pos (mem_Iic.1 hj)]

Premises used: Finset.mem_Iic, dif_pos, Iff.mp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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))

Tactic:
⟨fun h n _ ↦ h (Iic n), fun h I ↦ ?_⟩

Premises used: Iff.intro, Finset.Iic
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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 : ℕ
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
⊢ IsProjectiveLimit (α := X) ν μ ↔
    ∀ ⦃n : ℕ⦄,
      a ≤ n → Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))

Tactic:
refine ⟨fun h n _ ↦ h (Iic n), fun h I ↦ ?_⟩
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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 ℕ
⊢ 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)))
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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)
hf : Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (max (I.sup id) a)).restrict (π := X))
⊢ Measure.map (I.restrict (π := X)) ν = μ I

Tactic:
rw [← restrict₂_comp_restrict this, ← Measure.map_map, ← frestrictLe, h (le_max_right _ _), ← hμ]

Premises used: le_max_right, Finset.restrict₂_comp_restrict, Preorder.frestrictLe, MeasureTheory.Measure.map_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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)
⊢ Measurable.{u_1, u_1} (α := (i : ↥(Iic (max (I.sup id) a))) → X (↑i : ℕ)) (restrict₂ (π := X) this)

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
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)
⊢ Measurable.{u_1, u_1} (α := (i : ℕ) → X i) ((Iic (max (I.sup id) a)).restrict (π := X))

Tactic:
fun_prop
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
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))
⊢ IsProjectiveLimit (α := X) ν μ ↔
    ∀ (n : ℕ), Eq (α := Measure ((i : ↥(Iic n)) → X (↑i : ℕ))) (Measure.map (frestrictLe (π := X) n) ν) (μ (Iic n))

Tactic:
rw [isProjectiveLimit_nat_iff' hμ _ 0]

Premises used: OfNat.ofNat, MeasureTheory.isProjectiveLimit_nat_iff'
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X (↑i : ℕ))
hμ : IsProjectiveMeasureFamily (α := X) μ
ν : Measure ((n : ℕ) → X n)
⊢ (∀ ⦃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:
simp
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ_1 μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
inst_1 : ∀ (n : ℕ), SFinite (μ n)
I : Finset ℕ
⊢ SFinite (m0 := MeasurableSpace.pi (X := fun (k : ↥I) ↦ X (↑k : ℕ)))
    (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id)))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ_1 μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
inst_1 : ∀ (n : ℕ), IsFiniteMeasure (μ n)
I : Finset ℕ
⊢ IsFiniteMeasure (m0 := MeasurableSpace.pi (X := fun (k : ↥I) ↦ X (↑k : ℕ)))
    (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id)))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ_1 μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
inst_1 : ∀ (n : ℕ), IsZeroOrProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsZeroOrProbabilityMeasure (m0 := MeasurableSpace.pi (X := fun (k : ↥I) ↦ X (↑k : ℕ)))
    (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id)))

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ_1 μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
inst_1 : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (m0 := MeasurableSpace.pi (X := fun (k : ↥I) ↦ X (↑k : ℕ)))
    (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id)))

Tactic:
Measure.isProbabilityMeasure_map (measurable_restrict₂ _).aemeasurable

Premises used: Measurable.aemeasurable, Finset.measurable_restrict₂, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ_1 μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
inst_1 : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (m0 := MeasurableSpace.pi (X := fun (k : ↥I) ↦ X (↑k : ℕ)))
    (Measure.map (restrict₂ (π := X) ⋯) (μ (I.sup id)))

Tactic:
exact Measure.isProbabilityMeasure_map (measurable_restrict₂ _).aemeasurable

Premises used: Measurable.aemeasurable, Finset.measurable_restrict₂, MeasureTheory.Measure.isProbabilityMeasure_map
-- Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj
Goal:
X : ℕ → Type u_1
inst : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X (↑i : ℕ))
n : ℕ
rw :
  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)))
⊢ inducedFamily (X := X) μ (Iic n) = μ n

Tactic:
rw [inducedFamily, ← measure_cast (sup_Iic n) μ]

Premises used: MeasureTheory.inducedFamily, Finset.sup_Iic, _private.0.measure_cast