mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ deterministic (frestrictLe₂ hba) ⋯ = deterministic (frestrictLe₂ hba) ?inl✝

pp: case inl
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

pp: case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (restrict₂ ⋯)

pp: case inl.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

pp: case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)

Tactic:
]

Goal state after:
case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (restrict₂ ⋯)

case inl.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable Prod.fst

case inl.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
hba : b ≤ a
⊢ Measurable (frestrictLe₂ hba)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Kernel.id x = Kernel.id x

pp: case inr.base.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a a)

pp: case inr.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)

Tactic:
]

Goal state after:
case inr.base.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a a)

case inr.base
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b : ℕ
x : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ¬((κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∧ (κ.fst a) (countablePartitionSet n x) = 0 ∨
      (κ a) (countablePartitionSet n x ×ˢ univ) = ∞ ∧ (κ.fst a) (countablePartitionSet n x) ≠ ∞)

Tactic:
]

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ ¬((κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∧ (κ.fst a) (countablePartitionSet n x) = 0 ∨
      (κ a) (countablePartitionSet n x ×ˢ univ) = ∞ ∧ (κ.fst a) (countablePartitionSet n x) ≠ ∞)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))

Tactic:
]

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case e'_5
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ countablePartitionSet n x ×ˢ univ = countablePartitionSet n x ×ˢ univ

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
x : γ
hx : κ.densityProcess κ.fst n a x univ = 1
⊢ Tendsto (fun m ↦ κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
h : ∀ᵐ (a_1 : γ) ∂κ.fst a, ∀ (i : ℕ), κ.densityProcess κ.fst i a a_1 univ = 1
⊢ ∀ᵐ (x : γ) ∂κ.fst a, κ.density κ.fst a x univ = 1
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ))

Tactic:
]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ Tendsto (fun i ↦ ∫ (a_1 : γ), κ.density κ.fst a a_1 (seq i) ∂κ.fst a) atTop (𝓝 ((κ.fst a).real univ))
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ((κ a) {p | p.1 ∈ univ}).toReal = ((κ a) univ).toReal

Tactic:
]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
a : α
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
⊢ ((κ a) {p | p.1 ∈ univ}).toReal = ((κ a) univ).toReal
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) ((fun p ↦ {i | p i}) ⁻¹' {s | i ∈ s}) =
    (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True})

Tactic:
]

Goal state after:
ι : Type u_1
u : Set ι
p : ↑I
inst✝ : Countable ι
i : ι
hi : i ∉ u
⊢ (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) ((fun p ↦ {i | p i}) ⁻¹' {s | i ∈ s}) =
    (infinitePi fun i ↦ toNNReal p • dirac (i ∈ u) + toNNReal (σ p) • dirac False) (cylinder {i} {fun x ↦ True})
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case zero
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
⊢ x ⟨0, ⋯⟩ = x ⟨0, hj⟩

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case succ
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
⊢ (if h : j + 1 ≤ a then x ⟨j + 1, ⋯⟩ else ind j fun i ↦ iterateInduction x ind ↑i) = x ⟨j + 1, hj⟩

Tactic:
]

Goal state after:
case succ
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
⊢ (if h : j + 1 ≤ a then x ⟨j + 1, ⋯⟩ else ind j fun i ↦ iterateInduction x ind ↑i) = x ⟨j + 1, hj⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case succ
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
⊢ x ⟨j + 1, ⋯⟩ = x ⟨j + 1, hj⟩

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ setBer(u, p) {s_1 | s_1 ∈ Set.ncard ⁻¹' s ∧ s_1 ⊆ u} = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
s : Set ℕ
⊢ setBer(u, p) {s_1 | s_1 ∈ Set.ncard ⁻¹' s ∧ s_1 ⊆ u} = setBer(u, p) {t | t ⊆ u ∧ t.ncard ∈ s}
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ Finset.prod ?m.156 ?m.154 = ∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ x ∈ ?m.156, ((if x ∈ u ↔ x ∈ s then ↑(toNNReal p) else 0) + if x ∈ s then 0 else ↑(toNNReal (σ p))) = ?m.154 x

pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ Finset ι

pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ι → ℝ≥0∞

pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ b ∉ ?m.156, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1

Tactic:
]

Goal state after:
ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ x ∈ u,
    ((if x ∈ u ↔ x ∈ s then ↑(toNNReal p) else 0) + if x ∈ s then 0 else ↑(toNNReal (σ p))) =
      if x ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∀ b ∉ u, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ μ I = μ I

pp: case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

pp: case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict

Tactic:
]

Goal state after:
case hg
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (restrict₂ this)

case hf
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
a : ℕ
h : ∀ ⦃n : ℕ⦄, a ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)
I : Finset ℕ
this : I ⊆ Iic (max (I.sup id) a)
⊢ Measurable (Iic (max (I.sup id) a)).restrict
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ (∀ ⦃n : ℕ⦄, 0 ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)) ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (I : Finset ℕ) → Measure ((i : ↥I) → X ↑i)
hμ : IsProjectiveMeasureFamily μ
ν : Measure ((n : ℕ) → X n)
⊢ (∀ ⦃n : ℕ⦄, 0 ≤ n → Measure.map (frestrictLe n) ν = μ (Iic n)) ↔ ∀ (n : ℕ), Measure.map (frestrictLe n) ν = μ (Iic n)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), SFinite (μ n)
I : Finset ℕ
⊢ SFinite (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), SFinite (μ n)
I : Finset ℕ
⊢ SFinite (Measure.map (restrict₂ ⋯) (μ (I.sup id)))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsFiniteMeasure (μ n)
I : Finset ℕ
⊢ IsFiniteMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsFiniteMeasure (μ n)
I : Finset ℕ
⊢ IsFiniteMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsZeroOrProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsZeroOrProbabilityMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsZeroOrProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsZeroOrProbabilityMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
μ✝ μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
inst✝ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
I : Finset ℕ
⊢ IsProbabilityMeasure (Measure.map (restrict₂ ⋯) (μ (I.sup id)))
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real (⋃ x ∈ {t | t ⊆ u ∧ t.ncard ∈ {k}}, {x}) = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ setBer(u, p).real (⋃ x ∈ {t | t ⊆ u ∧ t.ncard ∈ {k}}, {x}) = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
n : ℕ
⊢ Measure.map (restrict₂ ⋯) (μ ((Iic n).sup id)) = Measure.map (cast ⋯) (μ ((Iic n).sup id))

Tactic:
]

Goal state after:
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure ((i : ↥(Iic n)) → X ↑i)
n : ℕ
⊢ Measure.map (restrict₂ ⋯) (μ ((Iic n).sup id)) = Measure.map (cast ⋯) (μ ((Iic n).sup id))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: 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 n) = ↑(Iic n)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case e_f
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)
⊢ x ⟨↑i, ⋯⟩ = x ⟨↑i, ⋯⟩

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ ∑ p_1 ∈ this.toFinset, setBer(u, p).real {p_1} = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
⊢ ∑ p_1 ∈ this.toFinset, setBer(u, p).real {p_1} = ↑(u.ncard.choose k) * ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
s : Set ι
hs : s ⊆ u ∧ s.ncard = k
⊢ ↑p ^ k * (1 - ↑p) ^ (u.ncard - k) = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)

Tactic:
]

Goal state after:
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: 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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measure.map (restrict₂ ⋯) (μ (J.sup id)) = Measure.map (restrict₂ ⋯) (μ (J.sup id))

pp: case hg
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

pp: case hf
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

pp: case hg
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ hJI)

pp: case hf
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

Tactic:
]

Goal state after:
case hg
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

case hf
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)

case hg
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ hJI)

case hf
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₂ hab) (μ b) = μ a
I J : Finset ℕ
hJI : J ⊆ I
sls : J.sup id ≤ I.sup id
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
h1 : ∀ s ∈ this.toFinset, setBer(u, p).real {s} = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
⊢ ↑{s | s ⊆ u ∧ s.ncard ∈ {k}}.ncard * (↑p ^ k * (1 - ↑p) ^ (u.ncard - k)) =
    ↑(u.ncard.choose k) * (↑p ^ k * (1 - ↑p) ^ (u.ncard - k))

Tactic:
]

Goal state after:
ι : Type u_1
inst✝ : Countable ι
u : Set ι
hu : u.Finite
p : ↑I
k : ℕ
this : {s | s ⊆ u ∧ s.ncard ∈ {k}}.Finite
h1 : ∀ s ∈ this.toFinset, setBer(u, p).real {s} = ↑p ^ k * (1 - ↑p) ^ (u.ncard - k)
⊢ ↑{s | s ⊆ u ∧ s.ncard ∈ {k}}.ncard * (↑p ^ k * (1 - ↑p) ^ (u.ncard - k)) =
    ↑(u.ncard.choose k) * (↑p ^ k * (1 - ↑p) ^ (u.ncard - k))
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
S : Set ((i : ↥(Iic b)) → X ↑i)
mS : MeasurableSet S
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ ((partialTraj κ a b) x₀) S = ((partialTraj κ a b) x₀) S

Tactic:
]

Goal state after: