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

Goal state before:
pp: α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) ρ) s = (ρ.fst ⊗ₘ ρ.condKernel.map f) s

Tactic:
conv_lhs => rw [← ρ.disintegrate ρ.condKernel]

Goal state after:
α : Type u_1
Ω : Type u_3
mα : MeasurableSpace α
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
ρ : Measure (α × Ω)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α Ω
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
f : Ω → ℝ := embeddingReal Ω
hf : MeasurableEmbedding (embeddingReal Ω)
ρ' : Measure (α × ℝ) := Measure.map (Prod.map id f) ρ
hρ'def : ρ' = Measure.map (Prod.map id f) ρ
hρ' : ρ'.fst = ρ.fst
hρ'' : ∀ᵐ (x : α) ∂ρ.fst, (κ.map f) x = ρ'.condKernel x
s : Set (α × ℝ)
hs : MeasurableSet s
⊢ (Measure.map (Prod.map id f) (ρ.fst ⊗ₘ ρ.condKernel)) s = (ρ.fst ⊗ₘ ρ.condKernel.map f) s
Module: Mathlib.Probability.Kernel.Integral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → β → E
s : Set α
a : α
⊢ ∫ (y : β), s.indicator (fun x ↦ f x y) a ∂κ a = s.indicator (fun x ↦ ∫ (y : β), f x y ∂κ x) a

Tactic:
by
  by_cases ha : a ∈ s <;> simp [ha]

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

Goal state before:
pp: case refine_2
α : 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 : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α), MeasurableSet s_1 → μ s_1 < ∞ → IntegrableOn (fun a ↦ ((condDistrib Y X μ) (X a)).real s) s_1 μ

pp: case refine_3
α : 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 : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ∞ →
        ∫ (x : α) in s_1, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ

pp: case refine_4
α : 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 : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ

Tactic:
· exact fun t _ _ => (integrable_toReal_condDistrib hX.aemeasurable hs).integrableOn

Goal state after:
case refine_3
α : 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 : Measurable Y
hs : MeasurableSet s
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      μ s_1 < ∞ →
        ∫ (x : α) in s_1, ((condDistrib Y X μ) (X x)).real s ∂μ = ∫ (x : α) in s_1, (Y ⁻¹' s).indicator (fun ω ↦ 1) x ∂μ

case refine_4
α : 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 : Measurable Y
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun a ↦ ((condDistrib Y X μ) (X a)).real s) μ
Module: Mathlib.Probability.Kernel.CondDistrib

Goal state before:
pp: 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)

Tactic:
· exact measurable_snd hs

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 ×ₖ (κ k).map ⇑(piSingleton k)).map (_root_.IicProdIoc k (k + 1)) ∘ₖ
      (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)).map (_root_.IicProdIoc a k) =
    (Kernel.id ×ₖ (partialTraj κ a (k + 1)).map (restrict₂ ⋯)).map (_root_.IicProdIoc a (k + 1))

Tactic:
comp_map,

Goal state after:
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 ×ₖ (κ k).map ⇑(piSingleton k)).map (_root_.IicProdIoc k (k + 1))).comap (_root_.IicProdIoc a k)
        ?inr.succ.hf ∘ₖ
      (Kernel.id ×ₖ (partialTraj κ a k).map (restrict₂ ⋯)) =
    (Kernel.id ×ₖ (partialTraj κ a (k + 1)).map (restrict₂ ⋯)).map (_root_.IicProdIoc a (k + 1))

case inr.succ.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsSFiniteKernel (κ n)
a b 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
⊢ Measurable (_root_.IicProdIoc a k)
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 | m] - μ[X | m] ^ 2) x ∂μ + (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), μ[X | m] x ∂μ) ^ 2) =
    ∫ (x : Ω), (X ^ 2) x ∂μ - ∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ +
      (∫ (x : Ω), (μ[X | m] ^ 2) x ∂μ - (∫ (x : Ω), X x ∂μ) ^ 2)

Tactic:
by
      rw [integral_sub' integrable_condExp, integral_condExp hm, integral_condExp hm]
      exact (hX.condExp one_le_two).integrable_sq

Goal state after:
Module: Mathlib.Probability.CondVar

Goal state before:
pp: Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
c : ℝ
X : Ω → ℝ
⊢ Var[c • X; μ | m] =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m]

Tactic:
by
      rw [condVar]
      refine condExp_congr_ae ?_
      filter_upwards [condExp_smul (m := m) c X] with ω hω
      simp [hω, ← mul_sub, mul_pow]

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 : γ
⊢ x ∈ κ.mutuallySingularSetSlice η a ↔ 1 ≤ κ.rnDerivAux (κ + η) a x

Tactic:
mutuallySingularSetSlice,

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ x ∈ {x | 1 ≤ κ.rnDerivAux (κ + η) a x} ↔ 1 ≤ κ.rnDerivAux (κ + η) a x
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 ∈ κ.mutuallySingularSetSlice η a

Tactic:
mutuallySingularSetSlice,

Goal state after:
α : 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}
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
hbc : b ≤ c
⊢ (partialTraj κ a c).map (frestrictLe₂ hbc) = partialTraj κ a b

Tactic:
by
  induction c, hbc using Nat.le_induction with
  | base => exact map_id ..
  | succ k h hk =>
    rw [← hk, ← frestrictLe₂_comp_frestrictLe₂ h k.le_succ, map_comp_right,
      partialTraj_succ_map_frestrictLe₂]
    all_goals fun_prop

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 α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (κ.singularPart η) a ⟂ₘ η a

Tactic:
by
  symm
  exact ⟨mutuallySingularSetSlice κ η a, measurableSet_mutuallySingularSetSlice κ η a,
    measure_mutuallySingularSetSlice κ η a, singularPart_compl_mutuallySingularSetSlice κ η a⟩

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

Goal state before:
pp: X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)

Tactic:
let g : ((i : Iic b) → X i) × (Π n, X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 _ c.1)

Goal state after:
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
a b : ℕ
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
g : ((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n) → ℝ≥0∞ := fun c ↦ f (updateFinset c.2 (Iic b) c.1)
⊢ Measurable fun x₀ ↦
    ∫⁻ (z : (i : ↥(Iic b)) → X ↑i), f (updateFinset x₀ (Iic b) z) ∂(partialTraj κ a b) (frestrictLe a x₀)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a ≤ (κ a) s

Tactic:
setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in s, (∂κ a/∂η a) x ∂η a ≤ (κ a) s
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (c : γ) in s, κ.rnDeriv η a c ∂η a = (κ a) s

Tactic:
setLIntegral_congr_fun_ae hs ((κ.rnDeriv_eq_rnDeriv_measure).mono (fun x hx _ ↦ hx)),

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : κ a ≪ η a
s : Set γ
hs : MeasurableSet s
⊢ ∫⁻ (x : γ) in s, (∂κ a/∂η a) x ∂η a = (κ a) s
Module: Mathlib.Probability.Kernel.Posterior

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
inst✝ : MeasurableSpace.CountablyGenerated 𝓧
f : Ω → 𝓧
hf : Measurable f
⊢ ⇑(Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) =ᵐ[Measure.map f μ] ⇑Kernel.id

Tactic:
refine Kernel.ae_eq_of_compProd_eq ?_
  calc μ.map f ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ)
  _ = (Kernel.deterministic f hf ∘ₘ μ)
      ⊗ₘ (Kernel.deterministic f hf ∘ₖ (Kernel.deterministic f hf)†μ) := by
    rw [Measure.deterministic_comp_eq_map]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.id ∥ₖ (Kernel.deterministic f hf)†μ) ∘ₘ
      Kernel.copy 𝓧 ∘ₘ Kernel.deterministic f hf ∘ₘ μ := by
    rw [Measure.compProd_eq_parallelComp_comp_copy_comp,
      ← Kernel.parallelComp_id_left_comp_parallelComp, ← Measure.comp_assoc]
  _ = (Kernel.id ∥ₖ Kernel.deterministic f hf) ∘ₘ (Kernel.deterministic f hf ∥ₖ Kernel.id) ∘ₘ
      Kernel.copy Ω ∘ₘ μ := by rw [parallelProd_posterior_comp_copy_comp]
  _ = (Kernel.deterministic f hf ∥ₖ Kernel.deterministic f hf) ∘ₘ Kernel.copy Ω ∘ₘ μ := by
    rw [Measure.comp_assoc, Kernel.parallelComp_comp_parallelComp, Kernel.id_comp, Kernel.comp_id]
  _ = (Kernel.copy 𝓧 ∘ₖ Kernel.deterministic f hf) ∘ₘ μ := by -- `deterministic` is used here
    rw [Measure.comp_assoc, Kernel.parallelComp_self_comp_copy]
  _ = μ.map f ⊗ₘ Kernel.id := by
    rw [Measure.compProd_id_eq_copy_comp, ← Measure.comp_assoc,
      Measure.deterministic_comp_eq_map]

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)
i : ι
⊢ map (Function.eval i) (infinitePi μ) = μ i

Tactic:
by
    ext s hs
    have : @Function.eval ι X i =
        (@Function.eval ({i} : Finset ι) (fun j ↦ X j) ⟨i, by simp⟩) ∘
        (Finset.restrict {i}) := by ext; simp
    rw [this, ← map_map, infinitePi_map_restrict, (measurePreserving_eval _ _).map_eq]
    all_goals fun_prop

Goal state after:
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
⊢ ∫⁻ (y : Θ), ∫⁻ (x : 𝓨), ℓ y x * (P y) Set.univ ∂μ ∂π = ∫⁻ (θ : Θ), (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ ∂π

Tactic:
congr with θ

Goal state after:
case e_f
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_4
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝² : Subsingleton 𝓧
inst✝¹ : Nonempty 𝓨
inst✝ : SFinite π
hl : Measurable (uncurry ℓ)
μ : Measure 𝓨
hμ : IsProbabilityMeasure μ
θ : Θ
⊢ ∫⁻ (x : 𝓨), ℓ θ x * (P θ) Set.univ ∂μ = (P θ) Set.univ * ∫⁻ (y : 𝓨), ℓ θ y ∂μ
Module: Mathlib.Probability.Distributions.Beta

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

Tactic:
compl_Ici,

Goal state after:
α β : ℝ
⊢ ∫⁻ (x : ℝ) in Iio 1, betaPDF α β x ∂volume.restrict (Ioi 0) =
    ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1))
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
⊢ cauchyPDF x₀ 0 = 0

Tactic:
by
  ext
  simp [cauchyPDF]

Goal state after:
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)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.155, gammaPDF a r x) + ∫⁻ (x : ℝ) in (Ici ?m.155)ᶜ, gammaPDF a r x).toReal = 1

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)))
⊢ ℝ

Tactic:
compl_Ici,

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)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.160, gammaPDF a r x) + ∫⁻ (x : ℝ) in Iio ?m.160, gammaPDF a r x).toReal = 1

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)))
⊢ ℝ
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hf
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)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

Tactic:
rw [EventuallyLE, ae_restrict_iff' measurableSet_Ici]
    exact ae_of_all _ (fun x (hx : 0 ≤ x) ↦ by positivity)

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

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.111, paretoPDF t r x) + ∫⁻ (x : ℝ) in (Ici ?m.111)ᶜ, paretoPDF t r x).toReal = 1

pp: t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ℝ

Tactic:
compl_Ici,

Goal state after:
t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ((∫⁻ (x : ℝ) in Ici ?m.116, paretoPDF t r x) + ∫⁻ (x : ℝ) in Iio ?m.116, paretoPDF t r x).toReal = 1

t r : ℝ
ht : 0 < t
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio t, paretoPDF t r x = 0
rightSide : ∫⁻ (x : ℝ) in Ici t, paretoPDF t r x = ∫⁻ (x : ℝ) in Ici t, ENNReal.ofReal (r * t ^ r * x ^ (-(r + 1)))
⊢ ℝ
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
s : Set β
⊢ (p.bind f).toOuterMeasure s = ∑' (a : α), p a * (f a).toOuterMeasure s

Tactic:
by
  classical
  calc
    (p.bind f).toOuterMeasure s = ∑' b, if b ∈ s then ∑' a, p a * f a b else 0 := by
      simp [toOuterMeasure_apply, Set.indicator_apply]
    _ = ∑' (b) (a), p a * if b ∈ s then f a b else 0 := tsum_congr fun b => by split_ifs <;> simp
    _ = ∑' (a) (b), p a * if b ∈ s then f a b else 0 := ENNReal.tsum_comm
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 := tsum_congr fun _ => ENNReal.tsum_mul_left
    _ = ∑' a, p a * ∑' b, if b ∈ s then f a b else 0 :=
      (tsum_congr fun a => (congr_arg fun x => p a * x) <| tsum_congr fun b => by split_ifs <;> rfl)
    _ = ∑' a, p a * (f a).toOuterMeasure s :=
      tsum_congr fun a => by simp only [toOuterMeasure_apply, Set.indicator_apply]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
⊢ (∑' (a_1 : β), p a * if h : p a = 0 then 0 else (f a h) a_1) = p a

Tactic:
simp_rw [ENNReal.tsum_mul_left]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
a : α
⊢ (p a * ∑' (i : β), if h : p a = 0 then 0 else (f a h) i) = p a
Module: Mathlib.Probability.ProbabilityMassFunction.Monad

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : p a' = 0
_ : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
⊢ p a' * 0 * 0 = p a' * 0

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : p a' = 0
_ : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
⊢ p a' * 0 * (g b ⋯) a = p a' * 0

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : (f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * 0)

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)

pp: case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * (g b ⋯) a)

Tactic:
any_goals ring1

Goal state after:
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
H : ¬(f a' h) b = 0
⊢ p a' * (f a' h) b * 0 = p a' * ((f a' h) b * (g b ⋯) a)

case pos
α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
f : (a : α) → a ∈ p.support → PMF β
g : (b : β) → b ∈ (p.bindOnSupport f).support → PMF γ
a : γ
a' : α
b : β
h : ¬p a' = 0
h_1 : ¬∀ (i : α), (p i * if h : p i = 0 then 0 else (f i h) b) = 0
h_2 : (f a' h) b = 0
⊢ p a' * (f a' h) b * (g b ⋯) a = p a' * ((f a' h) b * 0)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: case pos
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → ℝ
s : Set ℝ
huX : Measure.map X ℙ = (volume s)⁻¹ • volume.restrict s
hX : AEMeasurable X ℙ
⊢ ∫ (x : Ω), X x ∂ℙ = ∫ (x : ℝ), x ∂Measure.map X ℙ

Tactic:
exact (integral_map hX aestronglyMeasurable_id).symm

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h : Nonempty Ω
m : MeasurableSpace Ω
⊢ condExpKernel μ m = (condDistrib id id μ).comap id ⋯

Tactic:
simp [condExpKernel, h]

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
⊢ ⇑(condExpKernel μ m) ∘ₘ μ.trim hm = μ

Tactic:
rw [← Measure.snd_compProd, compProd_trim_condExpKernel]
  exact (@Measure.snd_map_prodMk Ω Ω Ω mΩ m mΩ id id μ (measurable_id'' hm)).trans Measure.map_id

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

Goal state before:
pp: Ω : Type u_1
F : Type u_2
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : IsFiniteMeasure μ
s : Set Ω
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
inst✝ : CompleteSpace F
hs : MeasurableSet s
f : Ω → F
hf : Integrable f μ
hμs : ¬μ s = 0
t : Set Ω
ht : MeasurableSet t
h : t = univ
⊢ μ s ≠ ∞

Tactic:
by finiteness

Goal state after: