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

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
⊢ (fun b ↦ ((borelMarkovFromReal Ω η) (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ.fst a] fun b ↦
    ((η.comapRight he) (a, b)) (Prod.mk b ⁻¹' t)

Tactic:
have h_ae : ∀ᵐ t ∂(fst κ a), (a, t) ∈ {p : α × β | η p (range e)ᶜ = 0} := by
    rw [← h_fst]
    have h_compProd : κ' a (univ ×ˢ range e)ᶜ = 0 := by
      unfold κ'
      rw [map_apply' _ (by fun_prop)]
      swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
      suffices Prod.map id e ⁻¹' (univ ×ˢ range e)ᶜ = ∅ by rw [this]; simp
      ext x
      simp
    rw [← hη', compProd_null] at h_compProd
    swap; · exact (MeasurableSet.univ.prod he.measurableSet_range).compl
    simp only [preimage_compl, mem_univ, mk_preimage_prod_right] at h_compProd
    exact h_compProd

Goal state after:
α : Type u_1
β : Type u_2
Ω : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
κ : Kernel α (β × Ω)
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) ℝ
inst✝ : IsSFiniteKernel η
hη : (κ.map (Prod.map id (embeddingReal Ω))).fst ⊗ₖ η = κ.map (Prod.map id (embeddingReal Ω))
e : Ω → ℝ := embeddingReal Ω
he : MeasurableEmbedding (embeddingReal Ω) := measurableEmbedding_embeddingReal Ω
κ' : Kernel α (β × ℝ) := κ.map (Prod.map id e)
hη' : κ'.fst ⊗ₖ η = κ'
h_prod_embed : MeasurableEmbedding (Prod.map id e)
h_fst : κ'.fst = κ.fst
a : α
t : Set (β × Ω)
ht : MeasurableSet t
h_ae : ∀ᵐ (t : β) ∂κ.fst a, (a, t) ∈ {p | (η p) (range e)ᶜ = 0}
⊢ (fun b ↦ ((borelMarkovFromReal Ω η) (a, b)) (Prod.mk b ⁻¹' t)) =ᵐ[κ.fst a] fun b ↦
    ((η.comapRight he) (a, b)) (Prod.mk b ⁻¹' t)
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: case refine_2
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
x✝ : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
⊢ x.2 ⟨i, ⋯⟩ ∈ s ⟨i, ⋯⟩

Tactic:
convert! h i hi2

Goal state after:
ι : Type u_1
inst✝³ : LinearOrder ι
inst✝² : LocallyFiniteOrder ι
inst✝¹ : DecidableLE ι
X : ι → Type u_2
inst✝ : LocallyFiniteOrderBot ι
a b : ι
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
x : ((i : ↥(Iic a)) → X ↑i) × ((i : ↥(Ioc a b)) → X ↑i)
h : ∀ (a_1 : ι) (b_1 : a_1 ≤ b), (if h : a_1 ≤ a then x.1 ⟨a_1, ⋯⟩ else x.2 ⟨a_1, ⋯⟩) ∈ s ⟨a_1, ⋯⟩
i : ι
x✝ : a < i ∧ i ≤ b
hi1 : a < i
hi2 : i ≤ b
⊢ x.2 ⟨i, ⋯⟩ = if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩
Module: Mathlib.Probability.Kernel.Disintegration.Unique

Goal state before:
pp: α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Kernel α (β × Ω)
inst✝¹ : IsFiniteKernel ρ
κ : Kernel (α × β) Ω
inst✝ : IsFiniteKernel κ
hκ : ρ.fst ⊗ₖ κ = ρ
a : α
⊢ (fun b ↦ κ (a, b)) =ᵐ[ρ.fst a] ⇑(ρ a).condKernel

Tactic:
by
  have : ρ a = (ρ a).fst ⊗ₘ Kernel.comap κ (fun b ↦ (a, b)) measurable_prodMk_left := by
    ext s hs
    conv_lhs => rw [← hκ]
    rw [Measure.compProd_apply hs, Kernel.compProd_apply hs]
    rfl
  have h := eq_condKernel_of_measure_eq_compProd _ this
  rw [Kernel.fst_apply]
  filter_upwards [h] with b hb
  rw [← hb, Kernel.comap_apply]

Goal state after:
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 ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ Antitone fun m ↦ univ ×ˢ seq m

pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∃ i, (κ a) (univ ×ˢ seq i) ≠ ∞

Tactic:
· exact antitone_const.set_prod hseq

Goal state after:
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
seq : ℕ → Set β
hseq : Antitone seq
hseq_iInter : ⋂ i, seq i = ∅
hseq_meas : ∀ (m : ℕ), MeasurableSet (seq m)
this : IsFiniteKernel κ
h_cont : ContinuousAt ENNReal.toReal 0
⊢ ∃ i, (κ a) (univ ×ˢ seq i) ≠ ∞
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 : (κ.fst a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m ↦ (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))

Tactic:
rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)] at h0 ⊢

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.IonescuTulcea.Traj

Goal state before:
pp: case hi
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)
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty (X m_1)
this : Nonempty ((i : ↥(Iic m)) → X ↑i)
⊢ Nonempty (X (m + 1))

Tactic:
exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
a : α
⊢ (κ.withDensity f) a ≪ κ a

Tactic:
by
  by_cases hf : Measurable (Function.uncurry f)
  · rw [Kernel.withDensity_apply _ hf]
    exact withDensity_absolutelyContinuous _ _
  · rw [withDensity_of_not_measurable _ hf]
    simp [Measure.AbsolutelyContinuous.zero]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
⊢ ∫⁻ (b : β) in s, (∑' (n : ι), f n) a b ∂κ a = ∫⁻ (b : β) in s, ∑' (n : ι), (fun b ↦ f n a b) b ∂κ a

Tactic:
congr with b

Goal state after:
case e_f
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝¹ : Countable ι
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : ι → α → β → ℝ≥0∞
hf : ∀ (i : ι), Measurable (Function.uncurry (f i))
h_sum_a : ∀ (a : α), Summable fun n ↦ f n a
h_sum : Summable fun n ↦ f n
a : α
s : Set β
hs : MeasurableSet s
b : β
⊢ (∑' (n : ι), f n) a b = ∑' (n : ι), (fun b ↦ f n a b) b
Module: Mathlib.Probability.Kernel.IonescuTulcea.Traj

Goal state before:
pp: case hi
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
A : ℕ → Set ((n : ℕ) → X n)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
p : ℕ
x₀ : (i : ↥(Iic p)) → X ↑i
m : ℕ
hm : ∀ m_1 ≤ m, Nonempty (X m_1)
this : Nonempty ((i : ↥(Iic m)) → X ↑i)
⊢ Nonempty (X (m + 1))

Tactic:
exact nonempty_of_isProbabilityMeasure (κ m Classical.ofNonempty)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsFiniteKernel κ
⊢ IsDeterministic κ ↔ ∀ (a : α), IsZeroOneMeasure (κ a)

Tactic:
constructor
  · intro h a
    refine ⟨fun s hs ↦ ?_⟩
    have := DFunLike.congr_fun κ.parallelComp_self_comp_copy a |> DFunLike.congr_fun
      <| (s ×ˢ s)
    rw [parallelComp_comp_copy, prod_apply_prod, copy_comp_apply_prod, inter_self] at this
    · by_cases hκ : κ a s = 0
      · simp [hκ]
      · exact Or.inr <| (ENNReal.mul_eq_left hκ (by simp)).mp this
    all_goals exact hs
  · intro _
    refine ⟨?_⟩
    ext : 1
    rw [parallelComp_comp_copy, prod_apply]
    refine Measure.prod_eq fun s t hs ht ↦ ?_
    rw [copy_comp_apply_prod _ _ hs ht]
    exact measure_inter_eq_prod hs ht

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

Goal state before:
pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable f (Measure.map (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀))

pp: case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀)

Tactic:
· convert! mf
    exact traj_map_updateFinset x₀

Goal state after:
case hg
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : AEMeasurable f ((traj κ a) x₀)
⊢ AEMeasurable (fun x ↦ updateFinset x (Iic a) x₀) ((traj κ a) x₀)
Module: Mathlib.Probability.Distributions.Bernoulli

Goal state before:
pp: X : Type u_1
inst✝¹ : MeasurableSpace X
x y : X
p : ↑I
s : Set X
hs : MeasurableSet s
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ Ber(x, y, p).real s = if x ∈ s then if y ∈ s then 1 else ↑(toNNReal p) else if y ∈ s then ↑(toNNReal (σ p)) else 0

Tactic:
by
  simp [measureReal_def, bernoulliMeasure_apply p hs, apply_ite ENNReal.toReal]

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

Goal state before:
pp: α β : ℝ
⊢ ∫⁻ (x : ℝ), betaPDF α β x = ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

Tactic:
← lintegral_add_compl _ measurableSet_Iic,

Goal state after:
α β : ℝ
⊢ (∫⁻ (x : ℝ) in Iic ?m.72, betaPDF α β x) + ∫⁻ (x : ℝ) in (Iic ?m.72)ᶜ, betaPDF α β x =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))

α β : ℝ
⊢ ℝ
Module: Mathlib.Probability.Distributions.Bernoulli

Goal state before:
pp: X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ ∫ (z : X), f z ∂Ber(x, y, p) = ↑p • f x + (1 - ↑p) • f y

Tactic:
rw [bernoulliMeasure_def, integral_add_measure]

Goal state after:
X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ ∫ (x : X), f x ∂toNNReal p • dirac x + ∫ (x : X), f x ∂toNNReal (σ p) • dirac y = ↑p • f x + (1 - ↑p) • f y

case hμ
X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f (toNNReal p • dirac x)

case hν
X : Type u_1
inst✝⁴ : MeasurableSpace X
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSingletonClass X
x y : X
p : ↑I
f : X → E
⊢ Integrable f (toNNReal (σ p) • dirac y)
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
inst✝ : CompleteSpace E
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_f : Integrable f ((traj κ a) x₀)
⊢ ((traj κ a) x₀)[f | ↑piLE b] =ᵐ[(traj κ a) x₀] fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) (frestrictLe b x)

Tactic:
by
  have i_f' : Integrable (fun x ↦ ∫ y, f y ∂(traj κ b) x)
      (((traj κ a) x₀).map (frestrictLe b)) := by
    rw [← map_apply _ (measurable_frestrictLe _), traj_map_frestrictLe _ _]
    rw [← traj_comp_partialTraj hab] at i_f
    exact i_f.integral_comp
  refine ae_eq_condExp_of_forall_setIntegral_eq (piLE.le _) i_f
    (fun s _ _ ↦ i_f'.comp_aemeasurable (measurable_frestrictLe b).aemeasurable |>.integrableOn)
    ?_ ?_ |>.symm <;> rw [piLE_eq_comap_frestrictLe]
  · rintro - ⟨t, mt, rfl⟩ -
    simp_rw [Function.comp_apply]
    rw [← setIntegral_map mt i_f'.1, ← map_apply, traj_map_frestrictLe,
      setIntegral_traj_partialTraj hab i_f mt]
    all_goals fun_prop
  · exact (i_f'.1.comp_ae_measurable' (measurable_frestrictLe b).aemeasurable)

Goal state after:
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
a : α
⊢ (p.filter s h) a = 0 ↔ a ∉ s ∨ a ∉ p.support

Tactic:
by
  rw [apply_eq_zero_iff, support_filter, Set.mem_inter_iff, not_and_or]

Goal state after:
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
s : Set (𝓧 × 𝓨)
hs : MeasurableSet s
⊢ (Measure.map (Prod.map f id) (Measure.map Z P ⊗ₘ κ.comap f hf)) s = (Measure.map f (Measure.map Z P) ⊗ₘ κ) s

Tactic:
rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply (by measurability),
          Measure.compProd_apply hs, lintegral_map (Kernel.measurable_kernel_prodMk_left hs) hf]

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
s : Set (𝓧 × 𝓨)
hs : MeasurableSet s
⊢ ∫⁻ (a : 𝓩), ((κ.comap f hf) a) (Prod.mk a ⁻¹' Prod.map f id ⁻¹' s) ∂Measure.map Z P =
    ∫⁻ (a : 𝓩), (κ (f a)) (Prod.mk (f a) ⁻¹' s) ∂Measure.map Z P
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hns : μ s ≠ 0
hnt : μ s ≠ ∞
hu : IsUniform X s ℙ μ
t : Set E := ⋯
⊢ Measure.map X ℙ = μ.withDensity (t.indicator ((μ t)⁻¹ • 1))

Tactic:
rw [hu, withDensity_indicator (measurableSet_toMeasurable μ s), withDensity_smul _ measurable_one,
    withDensity_one, restrict_toMeasurable hnt, measure_toMeasurable, ProbabilityTheory.cond]

Goal state after:
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']

Tactic:
specialize h s (sets := g) (fun i hi ↦ ?_)

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
h :
  ∀ (S : Finset ι) {sets : (i : ι) → Set (β i)},
    (∀ i ∈ S, MeasurableSet (sets i)) →
      μ[(⋂ i ∈ S, f i ⁻¹' sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ S, μ[(f i ⁻¹' sets i).indicator fun ω ↦ 1 | m']
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
i : ι
hi : i ∈ s
⊢ MeasurableSet (g i)

case refine_2
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
β : ι → Type u_5
m : (x : ι) → MeasurableSpace (β x)
f : (i : ι) → Ω → β i
hf : ∀ (i : ι), Measurable (f i)
s : Finset ι
sets : ι → Set Ω
h_sets : ∀ i ∈ s, MeasurableSet (sets i)
g : (i : ι) → Set (β i) := fun i ↦ if hi : i ∈ s then Exists.choose ⋯ else Set.univ
h : μ[(⋂ i ∈ s, f i ⁻¹' g i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i ⁻¹' g i).indicator fun ω ↦ 1 | m']
⊢ μ[(⋂ i ∈ s, sets i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(sets i).indicator fun ω ↦ 1 | m']
Module: Mathlib.Probability.ProbabilityMassFunction.Binomial

Goal state before:
pp: k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) =
    ↑x ^ k * ENNReal.ofReal (1 - ↑x) ^ (b - k) * ↑(b.choose k)

Tactic:
coe_nnreal_eq x,

Goal state after:
k b : ℕ
hb : k ≤ b
x : ℝ≥0
h : x ≤ 1
eq0 : k % (b + 1) = k
eq1 : 1 - ↑x = ENNReal.ofReal (1 - ↑x)
this : 1 - ↑x ≥ 0
⊢ ENNReal.ofReal (↑(b.choose k) * ↑x ^ k * (1 - ↑x) ^ (b - k)) =
    ENNReal.ofReal ↑x ^ k * ENNReal.ofReal (1 - ↑x) ^ (b - k) * ↑(b.choose k)
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q

Tactic:
convert! hX.IsKolmogorovProcess_mk.kolmogorovCondition s t using 1

Goal state after:
T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝¹ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q M
s t : T
⊢ ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P =
    ∫⁻ (ω : Ω), edist (IsAEKolmogorovProcess.mk X hX s ω) (IsAEKolmogorovProcess.mk X hX t ω) ^ p ∂P
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝³ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝² : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
hX : IsAEKolmogorovProcess X P p q M
s : T
⊢ X s =ᵐ[P] IsAEKolmogorovProcess.mk X hX s

Tactic:
filter_upwards [hX.ae_eq_mk s] with ω hω using hω

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun Y ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p
    (stoppedProcess (fun i ↦ {ω | ⊥ < τ ω}.indicator ({ω | ⊥ < Locally.localSeq hX n ω}.indicator (X i)))
      (τ ⊓ Locally.localSeq hX n))

Tactic:
stoppedProcess_indicator_comm',

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : LinearOrder ι
𝓕 : Filtration ι mΩ
p : (ι → Ω → E) → Prop
inst✝³ : OrderBot ι
inst✝² : Zero E
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
hp : IsStable 𝓕 p
X : ι → Ω → E
hX : (fun Y ↦ Locally p 𝓕 Y P) X
τ : Ω → WithTop ι
hτ : IsStoppingTime 𝓕 τ
n : ℕ
⊢ p fun i ↦
    {ω | ⊥ < τ ω}.indicator
      ({ω | ⊥ < Locally.localSeq hX n ω}.indicator (stoppedProcess X (τ ⊓ Locally.localSeq hX n) i))
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p (stoppedProcess (fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (X i)) fun ω ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j ω)

Tactic:
stoppedProcess_indicator_comm',

Goal state after:
ι : Type u_1
Ω : Type u_2
E : Type u_3
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁷ : ConditionallyCompleteLinearOrderBot ι
inst✝⁶ : TopologicalSpace ι
inst✝⁵ : OrderTopology ι
𝓕 : Filtration ι mΩ
X : ι → Ω → E
p : (ι → Ω → E) → Prop
inst✝⁴ : Zero E
inst✝³ : DenselyOrdered ι
inst✝² : FirstCountableTopology ι
inst✝¹ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
hp : IsStable 𝓕 p
inst✝ : 𝓕.IsRightContinuous
hτ : IsPreLocalizingSequence 𝓕 τ P
hpτ : ∀ (n : ℕ), p (stoppedProcess (fun i ↦ {ω | ⊥ < τ n ω}.indicator (X i)) (τ n))
n : ℕ
⊢ p fun i ↦ {ω | ⊥ < ⨅ j, ⨅ (_ : j ≥ n), τ j ω}.indicator (stoppedProcess X (fun ω ↦ ⨅ j, ⨅ (_ : j ≥ n), τ j ω) i)