mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.Process.HasIndepIncrements.Basic

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝² : Preorder T
inst✝¹ : MeasurableSpace E
inst✝ : Sub E
hX : HasIndepIncrements X P
r s t : T
hrs : r ≤ s
hst : s ≤ t
τ : ℕ → T :=
  fun x ↦
    match x with
    | 0 => r
    | 1 => s
    | x => t
⊢ (X s - X r) ⟂ᵢ[P] X t - X s

Tactic:
exact hX.nat (t := τ) (fun _ ↦ by grind) |>.indepFun (by grind : 0 ≠ 1)

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

Goal state before:
pp: α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | Monotone (f a)}

Tactic:
change MeasurableSet {a | ∀ q r (_ : q ≤ r), f a q ≤ f a r}

Goal state after:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : Measurable f
⊢ MeasurableSet {a | ∀ (q r : ℚ), q ≤ r → f a q ≤ f a r}
Module: Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes

Goal state before:
pp: case pos
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : p a
⊢ Tendsto (f a) atBot (𝓝 0)

pp: case neg
α : Type u_1
f g : α → ℚ → ℝ
a : α
p : α → Prop
inst✝ : DecidablePred p
hf : p a → IsRatStieltjesPoint f a
hg : ¬p a → IsRatStieltjesPoint g a
h : ¬p a
⊢ Tendsto (g a) atBot (𝓝 0)

Tactic:
exacts [(hf h).tendsto_atBot_zero, (hg h).tendsto_atBot_zero]

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

Goal state before:
pp: case h_directed
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
h_dir : Directed (fun x y ↦ x ⊆ y) fun q ↦ Iic ↑q
h_dir_prod : Directed (fun x y ↦ x ⊆ y) fun q ↦ s ×ˢ Iic ↑q
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i b ↦ ((IsCondKernelCDF.toKernel f hf) (a, b)) (Iic ↑i)

Tactic:
· refine Monotone.directed_le fun i j hij t ↦ measure_mono (Iic_subset_Iic.mpr ?_)
    exact mod_cast hij

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

Goal state before:
pp: case hg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ Measurable fun b ↦ ((IsCondKernelCDF.toKernel f hf) (a, b)) t

pp: case hg_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, a_1)) t ∂ν a ≠ ∞

pp: case h_le
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (fun b ↦ ((IsCondKernelCDF.toKernel f hf) (a, b)) t) ≤ᵐ[(ν a).restrict s] fun b ↦
    ((IsCondKernelCDF.toKernel f hf) (a, b)) univ

Tactic:
· exact (Kernel.measurable_coe (hf.toKernel f) ht).comp measurable_prodMk_left

Goal state after:
case hg_fin
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (a_1 : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, a_1)) t ∂ν a ≠ ∞

case h_le
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ (fun b ↦ ((IsCondKernelCDF.toKernel f hf) (a, b)) t) ≤ᵐ[(ν a).restrict s] fun b ↦
    ((IsCondKernelCDF.toKernel f hf) (a, b)) univ
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : t₁ ∈ {s | MeasurableSet s}
t₂ : Set ℝ
ht₂ : t₂ ∈ {t | MeasurableSet t}
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) t₁ t₂) ∂ν a =
    (κ a) ((fun x1 x2 ↦ x1 ×ˢ x2) t₁ t₂)

Tactic:
simp only [mem_ofPred_eq] at ht₁ ht₂

Goal state after:
case basic
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set (β × ℝ)
t₁ : Set β
ht₁ : MeasurableSet t₁
t₂ : Set ℝ
ht₂ : MeasurableSet t₂
⊢ ∫⁻ (b : β), ((IsCondKernelCDF.toKernel f hf) (a, b)) (Prod.mk b ⁻¹' (fun x1 x2 ↦ x1 ×ˢ x2) t₁ t₂) ∂ν a =
    (κ a) ((fun x1 x2 ↦ x1 ×ˢ x2) t₁ t₂)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case hm
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
this : IsFiniteKernel κ
S : Finset (Set γ)
hS_subset : ↑S ⊆ countablePartition γ n
hA : MeasurableSet (⋃₀ ↑S)
h_disj : Pairwise (Disjoint on fun i ↦ ↑i)
⊢ ∀ (i : ↑↑S), MeasurableSet ↑i

Tactic:
exact fun _ ↦ measurableSet_countablePartition n (hS_subset (by simp))

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

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
filter_upwards [this] with x hx
    ext t ht; exact hx ht

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

Goal state before:
pp: case neg
ι : Type u_1
inst✝⁴ : LinearOrder ι
inst✝³ : LocallyFiniteOrder ι
inst✝² : DecidableLE ι
X : ι → Type u_2
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : (i : ι) → MeasurableSpace (X i)
a b : ι
hab : a ≤ b
x : ↥(Iic b)
h : ¬↑x ≤ a
⊢ Measurable fun c ↦
    { toFun := fun x i ↦ if h : ↑i ≤ a then x.1 ⟨↑i, ⋯⟩ else x.2 ⟨↑i, ⋯⟩,
        invFun := fun x ↦ (fun i ↦ x ⟨↑i, ⋯⟩, fun i ↦ x ⟨↑i, ⋯⟩), left_inv := ⋯, right_inv := ⋯ }
      c x

Tactic:
simpa [h] using measurable_snd.eval

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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
s : Set Ω
hX : AEMeasurable X μ
hs : MeasurableSet s
⊢ Integrable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ

Tactic:
refine integrable_toReal_of_lintegral_ne_top ?_ ?_
  · exact Measurable.comp_aemeasurable (Kernel.measurable_coe _ hs) hX
  · refine ne_of_lt ?_
    calc
      ∫⁻ a, condDistrib Y X μ (X a) s ∂μ ≤ ∫⁻ _, 1 ∂μ := lintegral_mono fun a => prob_le_one
      _ = μ univ := lintegral_one
      _ < ∞ := measure_lt_top _ _

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

Goal state before:
pp: case hd
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
⊢ (countablePartition γ n).PairwiseDisjoint fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u

Tactic:
intro s hs t ht hst

Goal state after:
case hd
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
inst✝ : IsFiniteKernel κ
n : ℕ
a : α
this✝ : {x | ¬κ.densityProcess κ.fst n a x univ = 1} ⊆ {x | (κ.fst a) (countablePartitionSet n x) = 0}
this : {x | (κ.fst a) (countablePartitionSet n x) = 0} ⊆ ⋃ u ∈ countablePartition γ n, ⋃ (_ : (κ.fst a) u = 0), u
s : Set γ
hs : s ∈ countablePartition γ n
t : Set γ
ht : t ∈ countablePartition γ n
hst : s ≠ t
⊢ Function.onFun Disjoint (fun u ↦ ⋃ (_ : (κ.fst a) u = 0), u) s t
Module: Mathlib.Probability.Distributions.SetBernoulli

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∏ b ∈ ?m.145, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) =
    ∏ 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
⊢ ∀ b ∉ ?m.145, ((if b ∈ u ↔ b ∈ s then ↑(toNNReal p) else 0) + if b ∈ s then 0 else ↑(toNNReal (σ p))) = 1

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

Tactic:
Finset.prod_congr rfl

Goal state after:
ι : 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))

ι : 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

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

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

ι : 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
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_1
ι : 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 ∈ I \ J
⊢ (μ ↑⟨x, ⋯⟩) (if h : ↑⟨x, ⋯⟩ ∈ J then s ⟨↑⟨x, ⋯⟩, h⟩ else Set.univ) = 1

Tactic:
dif_neg (mem_sdiff.1 hx).2,

Goal state after:
case refine_1
ι : 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 ∈ I \ J
⊢ (μ ↑⟨x, ⋯⟩) Set.univ = 1
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_1
ι : 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 ∈ I \ J
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x = 1

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
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x

Tactic:
· rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]

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
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x
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_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ.withDensity f = Kernel.sum fun i ↦ (κ.seq i).withDensity f

Tactic:
← withDensity_kernel_sum _ _

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
⊢ κ.withDensity f = (Kernel.sum κ.seq).withDensity f
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inr
ι : 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
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_inf : Infinite ↑u
⊢ Tendsto (fun n ↦ (piContent fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)

Tactic:
have count_u : Countable u := Set.countable_iUnion (fun n ↦ (s n).countable_toSet)

Goal state after:
case inr
ι : 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
B_eq : ∀ (n : ℕ), B n = cylinder (t n) (T n)
mT : ∀ (n : ℕ), MeasurableSet (T n)
B_mem : ∀ (n : ℕ), B n ∈ measurableCylinders fun i ↦ X ↑i
mB : ∀ (n : ℕ), MeasurableSet (B n)
B_anti : Antitone B
B_inter : ⋂ n, B n = ∅
u_inf : Infinite ↑u
count_u : Countable ↑u
⊢ Tendsto (fun n ↦ (piContent fun i ↦ μ ↑i) (B n)) atTop (𝓝 0)
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ ν.prod μ
⊢ ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ

Tactic:
rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_compProd

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountableOrCountablyGenerated Ω 𝓧
h_ac : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : μ ⊗ₘ κ ≪ μ.prod (⇑κ ∘ₘ μ)
⊢ ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ

Tactic:
rw [← Measure.compProd_const] at this
    simpa using this.kernel_of_compProd

Goal state after:
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: case e_μ
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
inst✝⁴ : StandardBorelSpace Θ
inst✝³ : Nonempty Θ
hl : Measurable (Function.uncurry ℓ)
P : Kernel Θ 𝓧
inst✝² : IsFiniteKernel P
κ : Kernel 𝓧 𝓨
inst✝¹ : IsSFiniteKernel κ
π : Measure Θ
inst✝ : IsFiniteMeasure π
⊢ π ⊗ₘ (κ ∘ₖ P) = ⇑(P†π ×ₖ κ) ∘ₘ ⇑P ∘ₘ π

Tactic:
calc π ⊗ₘ (κ ∘ₖ P) = (Kernel.id ∥ₖ κ) ∘ₘ (π ⊗ₘ P) := Measure.parallelComp_comp_compProd.symm
  _ = (Kernel.id ∥ₖ κ) ∘ₘ ((P†π) ×ₖ Kernel.id) ∘ₘ P ∘ₘ π := by rw [posterior_prod_id_comp]
  _ = ((P†π) ×ₖ κ) ∘ₘ P ∘ₘ π := by
      rw [Measure.comp_assoc, Kernel.parallelComp_comp_prod, Kernel.id_comp, Kernel.comp_id]

Goal state after:
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)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) ((partialTraj κ a b) u ⊗ₘ traj κ b)

Tactic:
convert! hf.indicator (hA.prod .univ)

Goal state after:
case e'_6
X : ℕ → Type u_1
inst✝³ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝² : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ (uncurry fun x y ↦ A.indicator (fun x ↦ f x y) x) = (A ×ˢ Set.univ).indicator (uncurry f)
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Countable α
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSingletonClass α
p : PMF α
x : α
⊢ p.toMeasure.toPMF x = p x

Tactic:
rw [← p.toMeasure_apply_singleton x (measurableSet_singleton x), p.toMeasure.toPMF_apply]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) Po(r₁ + r₂) P

Tactic:
← poissonMeasure_conv_poissonMeasure

Goal state after:
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) (Po(r₁) ∗ Po(r₂)) P
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
r₁ r₂ : ℝ≥0
X Y : Ω → ℕ
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(r₁) P
hY : HasLaw Y Po(r₂) P
⊢ HasLaw (X + Y) Po(r₁ + r₂) P

Tactic:
rw [← poissonMeasure_conv_poissonMeasure]
  exact hXY.hasLaw_add hX hY

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
m mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
μ : Measure Ω
inst✝² : IsFiniteMeasure μ
inst✝¹ : NormedAddCommGroup F
f : Ω → F
inst✝ : NormedSpace ℝ F
hf : AEStronglyMeasurable f μ
a✝ : Nontrivial Ω
h : AEStronglyMeasurable (fun a ↦ ∫ (y : Ω), f (id a, y).2 ∂(condDistrib id id μ) (id a)) μ
⊢ AEStronglyMeasurable (fun ω ↦ ∫ (y : Ω), f y ∂((condDistrib id id μ).comap id ⋯) ω) μ

Tactic:
exact h.mono inf_le_left

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ : (((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t).toReal = μ[t | s].toReal
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]

Tactic:
ENNReal.toReal_eq_toReal_iff' (measure_ne_top _ t) (measure_ne_top _ t)

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsFiniteMeasure μ
s t : Set Ω
inst✝ : StandardBorelSpace Ω
hs : MeasurableSet s
ht : MeasurableSet t
this :
  (fun ω ↦ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω).real t) =ᵐ[μ.restrict s]
    μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}]
ω : Ω
hω₁ : μ[t.indicator fun ω ↦ 1 | MeasurableSpace.generateFrom {s}] ω = μ[|s].real t
hω₂ : ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
⊢ ((condExpKernel μ (MeasurableSpace.generateFrom {s})) ω) t = μ[t | s]
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case inr.h_le'
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ limsup s f ≤ m0

pp: case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ⨆ n ∈ ns i, s n

Tactic:
· exact limsup_le_iSup.trans (iSup_le h_le)

Goal state after:
case inr.hm
α : Type u_1
Ω : Type u_2
ι : Type u_3
_mα : MeasurableSpace α
s : ι → MeasurableSpace Ω
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
β : Type u_4
p : Set ι → Prop
f : Filter ι
ns : β → Set ι
h_le : ∀ (n : ι), s n ≤ m0
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hμ : μα ≠ 0
η : Kernel α Ω
η_eq : ⇑κ =ᵐ[μα] ⇑η
hη : IsMarkovKernel η
h_indep : iIndep s η μα
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ⨆ n ∈ ns i, s n