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

Goal state before:
pp: X : Type u_1
Y : Type u_2
E : Type u_3
mX : MeasurableSpace X
mY : MeasurableSpace Y
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
κ : Kernel X Y
μ : Measure X
f : X → Y → E
s : Set X
hs : MeasurableSet s
⊢ ∫ (x : X), ∫ (y : Y), s.indicator (fun x ↦ f x y) x ∂κ x ∂μ =
    ∫ (x : X), s.indicator (fun x ↦ ∫ (y : Y), f x y ∂κ x) x ∂μ

Tactic:
Kernel.integral_indicator₂

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

Goal state before:
pp: case pos
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.1.1 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.1.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.1 ⟨↑i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case pos
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩

Tactic:
rfl

Goal state after:
case pos
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).1 ⟨↑i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
x : (((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a k)) → X ↑i)) × ((i : ↥(Ioc k (k + 1))) → X ↑i)
i : ↥(Iic (k + 1))
h✝¹ : ¬↑i ≤ k
h✝ : ¬↑i ≤ a
⊢ x.2 ⟨↑i, ⋯⟩ = (prodAssoc x).2.2 ⟨↑i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case refl
X : ℕ → Type u_1
a : ℕ
⊢ ((i : ↥(Iic a)) → X ↑i) = ((i : ↥(Iic a)) → X ↑i)

Tactic:
rfl

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

Goal state before:
pp: case refl
X : ℕ → Type u_1
s : Set ℕ
x : (i : ↑s) → X ↑i
i : ↑s
⊢ cast ⋯ x i = x ⟨↑i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case refl
X : ℕ → Type u_1
inst✝ : (n : ℕ) → MeasurableSpace (X n)
a : ℕ
⊢ inferInstance ≍ inferInstance

Tactic:
rfl

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
S : Set (Set ι)
⊢ {s | s ∈ S ∧ s ⊆ u} ⊆ S

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
inst✝ : Countable ι
u : Set ι
p : ↑I
S : Set (Set ι)
⊢ S \ {s | s ∈ S ∧ s ⊆ u} ⊆ {x | (fun s ↦ s ⊆ u) x}ᶜ

Tactic:
grind

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 : ℕ
⊢ {s | s ⊆ u ∧ s.ncard ∈ {k}} ⊆ {b | b ⊆ u}

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∈ s
⊢ {t | t ∈ s ∧ t ⊆ ∅} = {∅}

Tactic:
grind

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

Goal state before:
pp: ι : Type u_1
p : ↑I
inst✝ : Countable ι
s : Set (Set ι)
hs : MeasurableSet s
h : ∅ ∉ s
⊢ {t | t ∈ s ∧ t ⊆ ∅} = ∅

Tactic:
grind

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) = (μ ↑⟨x, ⋯⟩) (if h : ↑⟨x, ⋯⟩ ∈ J then s ⟨↑⟨x, ⋯⟩, h⟩ else Set.univ)

Tactic:
dif_pos hx

Goal state after:
case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) = (μ ↑⟨x, ⋯⟩) (s ⟨↑⟨x, ⋯⟩, hx⟩)
Module: Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs

Goal state before:
pp: V : Type u_1
p : ↑I
inst✝ : Countable V
S : Set (SimpleGraph V)
⊢ G(V, p) S =
    (infinitePi fun e ↦ (toNNReal p • dirac ¬e.IsDiag) + toNNReal (σ p) • dirac False) ((fun G e ↦ e ∈ G.edgeSet) '' S)

Tactic:
by
  simp [binomialRandom_apply', setBernoulli_apply, ← Set.image_comp]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : Set ((i : ι) → X i)
hs : MeasurableSet s
e : ↥univ ≃ ι := { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
this : s = cylinder univ (⇑(piCongrLeft X e) ⁻¹' s)
⊢ (Measure.map (⇑(piCongrLeft X { toFun := fun i ↦ ↑i, invFun := fun i ↦ ⟨i, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }))
        (Measure.pi fun i ↦ μ ↑i))
      s =
    (Measure.map (⇑(piCongrLeft (fun i ↦ X i) e)) (Measure.pi fun i ↦ μ (e i))) s

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf : Measurable (Function.uncurry f)
a : α
⊢ { toFun := fun a ↦ (κ a).withDensity (f a), measurable' := ⋯ } a = (κ a).withDensity (f a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
⊢ Subsingleton ↥(Ioc n (n + 1))

Tactic:
rw [Nat.Ioc_succ_singleton]

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
inst✝ : ∀ (n : ℕ), SigmaFinite (μ n)
n : ℕ
s : (i : ↥(Ioc n (n + 1))) → Set (X ↑i)
hs : ∀ (i : ↥(Ioc n (n + 1))), MeasurableSet (s i)
⊢ Subsingleton ↥{n + 1}
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (x : β) in Set.univ, B ∂κ a = B * (κ a) Set.univ

Tactic:
by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
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 fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (updateFinset x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this : ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (f n) (update (updateFinset x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ ↑(Iic (k + 1))
h1 : i = k + 1
⊢ ⋯ ▸ x = ⋯ ▸ x

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
f : ℕ → ((n : ℕ) → X n) → ℝ≥0∞
a : ℕ → ℕ
hcte : ∀ (n : ℕ), DependsOn (f n) ↑(Iic (a n))
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 fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x
l : ((n : ℕ) → X n) → ℝ≥0∞
htendsto : ∀ (x : (n : ℕ) → X n), Tendsto (fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n) x) atTop (𝓝 (l x))
ε : ℝ≥0∞
y : (i : ↥(Iic k)) → X ↑i
hpos : ∀ (x : (i : ℕ) → X i) (n : ℕ), ε ≤ lmarginalPartialTraj κ k (a n) (f n) (updateFinset x (Iic k) y)
x✝ : ∀ (n : ℕ), Nonempty (X n)
F : ℕ → ((n : ℕ) → X n) → ℝ≥0∞ := fun n ↦ lmarginalPartialTraj κ (k + 1) (a n) (f n)
tendstoF : ∀ (x : (n : ℕ) → X n), Tendsto (fun x_1 ↦ F x_1 x) atTop (𝓝 (l x))
f_eq : ∀ (x : (n : ℕ) → X n) (n : ℕ), lmarginalPartialTraj κ k (a n) (f n) x = lmarginalPartialTraj κ k (k + 1) (F n) x
F_le : ∀ (n : ℕ) (x : (n : ℕ) → X n), F n x ≤ bound
tendsto_int :
  ∀ (x : (n : ℕ) → X n),
    Tendsto (fun n ↦ lmarginalPartialTraj κ k (a n) (f n) x) atTop (𝓝 (lmarginalPartialTraj κ k (k + 1) l x))
ε_le_lint : ∀ (x : (i : ℕ) → X i), ε ≤ lmarginalPartialTraj κ k (k + 1) l (updateFinset x (Iic k) y)
x_ : (n : ℕ) → X n := Classical.ofNonempty
x : X (k + 1)
hx : ε ≤ l (update (updateFinset x_ (Iic k) y) (k + 1) x)
x' : (i : ℕ) → X i
n : ℕ
this : ε ≤ lmarginalPartialTraj κ (k + 1) (a n) (f n) (update (updateFinset x_ (Iic k) y) (k + 1) x)
i : ℕ
hi : i ∈ ↑(Iic (k + 1))
h1 : ¬i = k + 1
h2 : i ≤ k
⊢ y ⟨i, ⋯⟩ = y ⟨i, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Kernel.WithDensity

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ f a b = (∑' (i : ℕ), fs i a) b

Tactic:
tsum_apply (h_sum_a a),

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ := fun n a b ↦ min (f a b) (↑n + 1) - min (f a b) ↑n
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable fun n ↦ fs n a
a : α
b : β
⊢ f a b = ∑' (i : ℕ), fs i a b
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
inst✝ : IsFiniteKernel η
hκη : κ ≤ η
a : α
⊢ κ.rnDerivAux η a ≤ᵐ[η a] 1

Tactic:
filter_upwards [Measure.rnDeriv_le_one_of_le (hκη a)] with x hx_le_one
  simp_rw [rnDerivAux]
  split_ifs with hα
  · refine ENNReal.toReal_le_of_le_ofReal zero_le_one ?_
    simp only [Pi.one_apply, ENNReal.ofReal_one]
    exact hx_le_one
  · have := hαγ.countableOrCountablyGenerated.resolve_left hα
    exact density_le_one ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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

Goal state before:
pp: case inr.succ
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 k : ℕ
h : a ≤ k
hk : partialTraj κ a k = (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k)
this :
  _root_.IicProdIoc k (k + 1) ∘ Prod.map (_root_.IicProdIoc a k) id =
    (⇑(MeasurableEquiv.IicProdIoc ⋯) ∘ Prod.map id (IocProdIoc a k (k + 1))) ∘ ⇑prodAssoc
⊢ Kernel.id ×ₖ
      ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k)).map (IocProdIoc a k (k + 1) ∘ Prod.map (restrict₂ ⋯) id) ∘ₖ
        partialTraj κ a k) =
    Kernel.id ×ₖ
      ((Kernel.id ×ₖ (κ k).map ⇑(piSingleton k)).map (restrict₂ ⋯ ∘ _root_.IicProdIoc k (k + 1)) ∘ₖ partialTraj κ a k)

Tactic:
rfl

Goal state after:
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ (a, x) ∈ {p | 1 ≤ κ.rnDerivAux (κ + η) p.1 p.2} ↔ x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x}

Tactic:
mem_ofPred,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ 1 ≤ κ.rnDerivAux (κ + η) (a, x).1 (a, x).2 ↔ x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x}
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
g : (n : ℕ) → ((a : ↥(t n)) → X ↑((aux n) a)) ≃ ((b : ↥(s n)) → X ↑b) :=
  fun n ↦ Equiv.piCongrLeft (fun i ↦ X ↑i) (aux n)
r_comp_f : ∀ (n : ℕ), (s n).restrict ∘ f = ⇑(g n) ∘ fun x i ↦ x ↑i
B : ℕ → Set ((i : ↑u) → X ↑i) := fun n ↦ f ⁻¹' A n
T : (n : ℕ) → Set ((a : ↥(t n)) → X ↑((aux n) a)) := fun n ↦ ⇑(g n) ⁻¹' S n
n : ℕ
⊢ (⇑(g n) ∘ fun x i ↦ x ↑i) ⁻¹' S n = (t n).restrict ⁻¹' T n

Tactic:
rfl

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

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

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : i ≤ a
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩

Tactic:
rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : i ≤ a
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : i ≤ a
h✝ : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : ¬i ≤ a
h✝ : a < i ∧ i ≤ b
⊢ x✝ ⟨i, ⋯⟩ = x✝ ⟨i, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : ¬i ≤ a
h✝ : ¬(a < i ∧ i ≤ b)
⊢ x✝ ⟨i, ⋯⟩ = x₀ i

Tactic:
rfl

Goal state after:
case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝² : i ≤ b
h✝¹ : ¬i ≤ a
h✝ : ¬(a < i ∧ i ≤ b)
⊢ x✝ ⟨i, ⋯⟩ = x₀ i
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝¹ : ¬i ≤ b
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩

Tactic:
rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝¹ : ¬i ≤ b
h✝ : a < i ∧ i ≤ b
⊢ x₀ i = x✝ ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x✝ : (i : ↥(Ioc a b)) → X ↑i
i : ℕ
h✝¹ : ¬i ≤ b
h✝ : ¬(a < i ∧ i ≤ b)
⊢ x₀ i = x₀ i

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : i ≤ a
h3 : i = a + 1
⊢ x₀ i = ⋯ ▸ x

Tactic:
rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : i ≤ a
h3 : i = a + 1
⊢ x₀ i = ⋯ ▸ x
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : i ≤ a
h3 : ¬i = a + 1
⊢ x₀ i = x₀ i

Tactic:
rfl

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

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : ¬i ≤ a
h✝ : i = a + 1
⊢ { toFun := fun x i ↦ ⋯ ▸ x, invFun := fun x ↦ x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x ⟨i, ⋯⟩ = ⋯ ▸ x

Tactic:
rfl

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

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : ¬i ≤ a
h✝ : ¬i = a + 1
⊢ { toFun := fun x i ↦ ⋯ ▸ x, invFun := fun x ↦ x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x ⟨i, ⋯⟩ = x₀ i

Tactic:
rfl

Goal state after:
case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : i ≤ a + 1
h2 : ¬i ≤ a
h✝ : ¬i = a + 1
⊢ { toFun := fun x i ↦ ⋯ ▸ x, invFun := fun x ↦ x ⟨a + 1, ⋯⟩, left_inv := ⋯, right_inv := ⋯ } x ⟨i, ⋯⟩ = x₀ i
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : ¬i ≤ a + 1
h✝ : i = a + 1
⊢ x₀ i = ⋯ ▸ x

Tactic:
rfl

Goal state after:
case pos
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : ¬i ≤ a + 1
h✝ : i = a + 1
⊢ x₀ i = ⋯ ▸ x
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case neg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
x₀ : (n : ℕ) → X n
x : X (a + 1)
i : ℕ
h1 : ¬i ≤ a + 1
h✝ : ¬i = a + 1
⊢ x₀ i = x₀ i

Tactic:
rfl

Goal state after: