mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
h_univ : Set.univ = ⋃ a, {x | ‖x‖ ≤ ↑a}
a : ℕ
⊢ ∀ ⦃b : ℕ⦄, a ≤ b → (fun a ↦ {x | ‖x‖ ≤ ↑a}) a ⊆ (fun a ↦ {x | ‖x‖ ≤ ↑a}) b

Tactic:
b

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsProbabilityMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
h_meas_Ioo : ∀ (a : ℝ), 0 < a → 2⁻¹ < μ {x | ‖x‖ ≤ a} → 1 ≤ μ {x | ‖x‖ ≤ a}
h_ne : ∀ (b : ℝ), μ {x | ‖x‖ ≤ b} ≠ 1
h_le : ∀ (a : ℝ), μ {x | ‖x‖ ≤ a} ≤ 2⁻¹
h_univ : Set.univ = ⋃ a, {x | ‖x‖ ≤ ↑a}
a b : ℕ
⊢ a ≤ b → (fun a ↦ {x | ‖x‖ ≤ ↑a}) a ⊆ (fun a ↦ {x | ‖x‖ ≤ ↑a}) b
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : μ = 0
⊢ Integrable (fun x ↦ rexp (1 * ‖x‖ ^ 2)) μ

Tactic:
by simp [hμ_zero]

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

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h_rot : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
hμ_zero : ¬μ = 0
μ' : Measure E := μ[|Set.univ]
hμ'_eq : μ' = (μ Set.univ)⁻¹ • μ
⊢ μ Set.univ ≠ 0

Tactic:
by simp [hμ_zero]

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

Goal state before:
pp: case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ 1 ≤ if ↑x < 0 then 0 else 1

Tactic:
if_neg

Goal state after:
case neg.refine_2
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ 1 ≤ 1

case neg.refine_2.hnc
t : ℚ
h_bdd : BddBelow (range fun r ↦ if ↑r < 0 then 0 else 1)
h : ¬t < 0
x : ↑(Ioi t)
⊢ ¬↑x < 0
Module: Mathlib.Probability.Kernel.Disintegration.CondCDF

Goal state before:
pp: α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ Measurable fun a r ↦ (preCDF ρ r a).toReal

Tactic:
measurable_pi_iff

Goal state after:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
⊢ ∀ (a : ℚ), Measurable fun x ↦ (preCDF ρ a x).toReal
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : Measurable f := hf.measurable
⊢ Measurable fun t ↦ f (a, t) q

Tactic:
measurable_pi_iff

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
a : α
q : ℚ
h : ∀ (a : ℚ), Measurable fun x ↦ f x a
⊢ Measurable fun t ↦ f (a, t) q
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
a✝ : (ν a) s < ∞
⊢ ∫ (x : β) in s, ⨅ r, f (a, x) ↑r ∂ν a = (κ a).real (s ×ˢ Iic ↑q)

Tactic:
hf.setIntegral_iInf_rat_gt _ _ hs

Goal state after:
case refine_3
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
q : ℚ
s : Set β
hs : MeasurableSet s
a✝ : (ν a) s < ∞
⊢ (κ a).real (s ×ˢ Iic ↑q) = (κ a).real (s ×ˢ Iic ↑q)
Module: Mathlib.Probability.Kernel.Disintegration.CDFToKernel

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, IsRatStieltjesPoint f (a, t)

Tactic:
filter_upwards [hf.tendsto_atTop_one a, hf.tendsto_atBot_zero a,
    hf.iInf_rat_gt_eq a, hf.mono a] with t ht_top ht_bot ht_iInf h_mono
  exact ⟨h_mono, ht_top, ht_bot, ht_iInf⟩

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.Lemmas

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = (⇑(Kernel.id ∥ₖ κ) ∘ₘ μ.prod ν) s

Tactic:
Measure.bind_apply hs (Kernel.aemeasurable _)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
μ : Measure α
ν : Measure β
inst✝¹ : SFinite ν
κ : Kernel β γ
inst✝ : IsSFiniteKernel κ
s : Set (α × γ)
hs : MeasurableSet s
⊢ ∫⁻ (x : α), (⇑κ ∘ₘ ν) (Prod.mk x ⁻¹' s) ∂μ = ∫⁻ (a : α × β), ((Kernel.id ∥ₖ κ) a) s ∂μ.prod ν
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
⊢ (∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1) ∧ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ

Tactic:
have h_eq s (hs : MeasurableSet s) :
      ∫⁻ b, s.indicator (fun b ↦ κCond (a, b) Set.univ) b ∂κ.fst a = κ.fst a s := by
    conv_rhs => rw [← h]
    rw [fst_compProd_apply _ _ _ hs]

Goal state after:
case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mΩ : MeasurableSpace Ω
κ : Kernel α (β × Ω)
κCond : Kernel (α × β) Ω
inst✝¹ : IsFiniteKernel κ.fst
inst✝ : κ.IsCondKernel κCond
a : α
h : κ.fst ⊗ₖ κCond = κ
h_sfin : IsSFiniteKernel κCond
h_eq : ∀ (s : Set β), MeasurableSet s → ∫⁻ (b : β), s.indicator (fun b ↦ (κCond (a, b)) univ) b ∂κ.fst a = (κ.fst a) s
⊢ (∀ᵐ (b : β) ∂κ.fst a, (κCond (a, b)) univ ≤ 1) ∧ ∀ᵐ (b : β) ∂κ.fst a, 1 ≤ (κCond (a, b)) univ
Module: Mathlib.Probability.Kernel.Disintegration.StandardBorel

Goal state before:
pp: case pos
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h : (η a) (range (embeddingReal Ω))ᶜ = 0
⊢ (Measure.comap (embeddingReal Ω) (η a)) s = (η a) (embeddingReal Ω '' s)

Tactic:
Measure.comap_apply _ he.injective he.measurableSet_image' _ hs

Goal state after:
case pos
α : Type u_1
mα : MeasurableSpace α
Ω : Type u_5
inst✝² : Nonempty Ω
inst✝¹ : MeasurableSpace Ω
inst✝ : StandardBorelSpace Ω
η : Kernel α ℝ
a : α
s : Set Ω
hs : MeasurableSet s
he : MeasurableEmbedding (embeddingReal Ω)
h : (η a) (range (embeddingReal Ω))ᶜ = 0
⊢ (η a) (embeddingReal Ω '' s) = (η a) (embeddingReal Ω '' s)
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
x : γ
⊢ ‖κ.densityProcess ν n a x s‖₊ ≤ 1

Tactic:
rw [Real.nnnorm_of_nonneg (densityProcess_nonneg _ _ _ _ _ _)]

Goal state after:
case refine_2.refine_2.refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
ε : ℝ
x✝ : 0 < ε
n : ℕ
x : γ
⊢ NNReal.mk (κ.densityProcess ν n a x s) ⋯ ≤ 1
Module: Mathlib.Probability.Kernel.IonescuTulcea.Maps

Goal state before:
pp: ι : 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 : ι
hi : i ≤ a
⊢ x.1 ⟨i, ⋯⟩ = if h : i ≤ a then x.1 ⟨i, ⋯⟩ else x.2 ⟨i, ⋯⟩

Tactic:
rw [dif_pos hi]

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 : Measurable X
hY : AEMeasurable Y μ
hs : MeasurableSet s
t' : Set β
ht' : MeasurableSet t'
⊢ ∫⁻ (a : α) in X ⁻¹' t', ((condDistrib Y X μ) (X a)) s ∂μ = μ (X ⁻¹' t' ∩ Y ⁻¹' s)

Tactic:
rw [setLIntegral_preimage_condDistrib hX hY hs ht']

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (a : α) in X ⁻¹' t, ∫ (y : Ω), f (X a, y) ∂(condDistrib Y X μ) (X a) ∂μ = ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

Tactic:
← integral_map hX.aemeasurable (f := fun x' => ∫ y, f (x', y) ∂(condDistrib Y X μ) x')

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ ∫ (y : β), ∫ (y_1 : Ω), f (y, y_1) ∂(condDistrib Y X μ) y ∂Measure.map X (μ.restrict (X ⁻¹' t)) =
    ∫ (a : α) in X ⁻¹' t, f (X a, Y a) ∂μ

case refine_2
α : Type u_1
β : Type u_2
Ω : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace Ω
inst✝⁵ : StandardBorelSpace Ω
inst✝⁴ : Nonempty Ω
inst✝³ : NormedAddCommGroup F
mα : MeasurableSpace α
μ : Measure α
inst✝² : IsFiniteMeasure μ
X : α → β
Y : α → Ω
mβ : MeasurableSpace β
f : β × Ω → F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hX : Measurable X
hY : AEMeasurable Y μ
hf_int : Integrable f (Measure.map (fun a ↦ (X a, Y a)) μ)
hf_int' : Integrable (fun a ↦ f (X a, Y a)) μ
t : Set β
ht : MeasurableSet t
a✝ : μ (X ⁻¹' t) < ∞
⊢ AEStronglyMeasurable (fun x' ↦ ∫ (y : Ω), f (x', y) ∂(condDistrib Y X μ) x') (Measure.map X (μ.restrict (X ⁻¹' t)))
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ (Measure.map (fun ω ↦ (X ω, ω)) μ) (Prod.snd ⁻¹' s) = 0

Tactic:
Measure.map_apply_of_aemeasurable

Goal state after:
case pos
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ μ ((fun ω ↦ (X ω, ω)) ⁻¹' Prod.snd ⁻¹' s) = 0

case pos.hf
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ AEMeasurable (fun ω ↦ (X ω, ω)) μ

case pos.hs
β : Type u_2
mβ : MeasurableSpace β
Ω : Type u_5
F : Type u_6
mΩ : MeasurableSpace Ω
X : Ω → β
μ : Measure Ω
inst✝ : TopologicalSpace F
f : Ω → F
hf : AEStronglyMeasurable f μ
s : Set Ω
hs : MeasurableSet s
hμs : μ s = 0
hX : AEMeasurable X μ
⊢ MeasurableSet (Prod.snd ⁻¹' s)
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 α (γ × β)
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
h : (κ.fst a) s = 0
⊢ MeasurableSet (⋃ (_ : (κ.fst a) s = 0), s)

Tactic:
simp [h, measurableSet_countablePartition n hs]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: case pos
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
hμm : IsFiniteMeasure μ
⊢ Var[fun x ↦ c; μ | m] = 0

Tactic:
simp [condVar, hm]

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst✝ : IsProbabilityMeasure μ
hX : MemLp X 2 μ
⊢ ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2) =
    Var[X; μ]

Tactic:
by rw [variance_eq_sub hX]; ring

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 β
κ✝ : Kernel α β
f✝ : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : α → β → ℝ≥0∞
hf : Measurable (Function.uncurry f)
⊢ Measurable fun a ↦ (κ a).withDensity (f a)

Tactic:
by
        refine Measure.measurable_of_measurable_coe _ fun s hs => ?_
        simp_rw [withDensity_apply _ hs]
        exact hf.setLIntegral_kernel_prod_right hs

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)
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, ε ≤ l (update (updateFinset x_ (Iic k) y) (k + 1) x)

Tactic:
by
    have : ∫⁻ x, l (update (updateFinset x_ _ y) (k + 1) x) ∂(κ k y) ≠ ∞ :=
      ne_top_of_le_ne_top fin_bound <| lintegral_le_const <| ae_of_all _
        fun y ↦ le_of_tendsto' (tendstoF _) <| fun _ ↦ F_le _ _
    obtain ⟨x, hx⟩ := exists_lintegral_le this
    refine ⟨x, (ε_le_lint x_).trans ?_⟩
    rwa [lmarginalPartialTraj_succ, frestrictLe_updateFinset]
    exact ENNReal.measurable_of_tendsto (by fun_prop) (tendsto_pi_nhds.2 htendsto)

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
a : α
⊢ ∀ (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n

Tactic:
b

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
a : α
b : β
⊢ ∀ (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ ↑n
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
a : α
⊢ ∀ (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0

Tactic:
b

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
a : α
b : β
⊢ ∀ (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η ξ : Kernel α γ
f : α → γ → ℝ≥0∞
inst✝ : IsFiniteKernel η
h : κ = η.withDensity f + ξ
hf : Measurable (Function.uncurry f)
a : α
hξ : ξ a ⟂ₘ η a
this : κ a = ξ a + (η a).withDensity (f a)
⊢ ξ a = (κ a).singularPart (η a)

Tactic:
exact (κ a).eq_singularPart (hf.comp measurable_prodMk_left) hξ this

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

Goal state before:
pp: case refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
c : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
mf : Measurable f
hf : DependsOn f ↑(Iic a)
hab : a ≤ b
x : (n : ℕ) → X n
⊢ IsMarkovKernel ((partialTraj κ b c).map (restrict₂ ⋯))

Tactic:
exact IsMarkovKernel.map _ (by fun_prop)

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
η : Kernel 𝓧 𝓨
inst✝ : IsFiniteKernel η
⊢ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ =
    ⇑(η ∥ₖ Kernel.id) ∘ₘ ⇑(Kernel.id ∥ₖ κ†μ) ∘ₘ ⇑(Kernel.copy 𝓧) ∘ₘ ⇑κ ∘ₘ μ

Tactic:
rw [Measure.comp_assoc, Kernel.parallelComp_comm, ← Measure.comp_assoc]

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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x ω = κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x

Tactic:
convert!
    Measure.ae_ae_of_ae_prod
      (rnDeriv_posterior_ae_prod h_ac)

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✝ : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → ℝ≥0∞ := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ ∫⁻ (y : (i : ι) → X i), f y ∂infinitePi μ = (∫⋯∫⁻_s, f ∂μ) x

Tactic:
← lintegral_congr_ae <| ae_of_all _ this,

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : DecidableEq ι
s : Finset ι
f : ((i : ι) → X i) → ℝ≥0∞
mf : Measurable f
x : (i : ι) → X i
g : ((i : ↥s) → X ↑i) → ℝ≥0∞ := fun y ↦ f (Function.updateFinset x s y)
this : ∀ (y : (i : ι) → X i), g (s.restrict y) = f y
⊢ ∫⁻ (a : (i : ι) → X i), g (s.restrict a) ∂infinitePi μ = (∫⋯∫⁻_s, f ∂μ) x
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ r ^ a * (1 / r) ^ a * (Gamma a / Gamma a) = 1

Tactic:
div_self (Gamma_pos_of_pos ha).ne',

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ r ^ a * (1 / r) ^ a * 1 = 1
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
a : α
⊢ p a = 0 ↔ a ∉ p.support

Tactic:
by
  rw [mem_support_iff, Classical.not_not]

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

Goal state before:
pp: case refine_1
α : Type u_1
p : PMF α
s : Set α
h : ∑' (x : α), s.indicator (⇑p) x = 1
a : α
hap : a ∈ p.support
⊢ a ∈ s

Tactic:
refine by_contra fun hs => ne_of_lt ?_ (h.trans p.tsum_coe.symm)
    have hs' : s.indicator p a = 0 := Set.indicator_apply_eq_zero.2 fun hs' => False.elim <| hs hs'
    have hsa : s.indicator p a < p a := hs'.symm ▸ (p.apply_pos_iff a).2 hap
    exact ENNReal.tsum_lt_tsum (p.tsum_coe_indicator_ne_top s)
      (fun x => Set.indicator_apply_le fun _ => le_rfl) hsa

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

Goal state before:
pp: case false
p : ℝ≥0
h : p ≤ 1
⊢ false ∈ (bernoulli p h).support ↔ false ∈ {b | bif b then p ≠ 0 else p ≠ 1}

pp: case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}

Tactic:
· simp_rw [mem_support_iff, bernoulli_apply, Bool.cond_false, Ne, ENNReal.coe_sub,
      ENNReal.coe_one, Bool.cond_prop, Set.mem_ofPred_eq, Bool.false_eq_true, ite_false,
      not_iff_not]
    constructor
    · intro h'
      simp only [tsub_eq_zero_iff_le, one_le_coe_iff] at h'
      exact eq_of_le_of_ge h h'
    · intro h'
      simp only [h', ENNReal.coe_one, tsub_self]

Goal state after:
case true
p : ℝ≥0
h : p ≤ 1
⊢ true ∈ (bernoulli p h).support ↔ true ∈ {b | bif b then p ≠ 0 else p ≠ 1}