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

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
Function.extend_val_apply hx,

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
Function.extend_val_apply hx,

Goal state after:
case e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
s : (i : ↥(Ioc a c)) → Set (X ↑i)
ms : ∀ (i : ↥(Ioc a c)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc b c
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)
Module: Mathlib.Probability.Decision.Risk.Defs

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Nonempty 𝓧
inst✝ : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero

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

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsEmpty 𝓨
⊢ ∀ (x : Kernel 𝓧 𝓨), ¬IsMarkovKernel x

Tactic:
exact fun κ ↦ Subsingleton.elim κ 0 ▸ Kernel.not_isMarkovKernel_zero

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (frestrictLe₂ hab s i)) 1 x

Tactic:
Function.extend_val_apply hx,

Goal state after:
case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Iic a
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x = (μ ↑⟨x, hx⟩) (frestrictLe₂ hab s ⟨x, hx⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (restrict₂ ⋯ s i)) 1 x

Tactic:
Function.extend_val_apply hx,

Goal state after:
case inl.e_a
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a ≤ b
s : (i : ↥(Iic b)) → Set (X ↑i)
ms : ∀ (i : ↥(Iic b)), MeasurableSet (s i)
x : ℕ
hx : x ∈ Ioc a b
⊢ Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x = (μ ↑⟨x, hx⟩) (restrict₂ ⋯ s ⟨x, hx⟩)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measure.map (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1))
      ((Kernel.id x₀).prod (Measure.map (⇑(piSingleton a)) (μ (a + 1)))) =
    Measure.pi fun i ↦ μ ↑i

pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable ⇑(piSingleton a)

pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1))

pp: case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a (a + 1))

pp: case inl.refine_1.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)

Tactic:
Measure.map_piSingleton,

Goal state after:
case inl.refine_1
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measure.map (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1)) ((Kernel.id x₀).prod (Measure.pi fun i ↦ μ ↑i)) =
    Measure.pi fun i ↦ μ ↑i

case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable ⇑(piSingleton a)

case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯ ∘ _root_.IicProdIoc a (a + 1))

case inl.refine_1.hf
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (_root_.IicProdIoc a (a + 1))

case inl.refine_1.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
μ : (n : ℕ) → Measure (X n)
hμ : ∀ (n : ℕ), IsProbabilityMeasure (μ n)
a b : ℕ
hab : a < b
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ Measurable (restrict₂ ⋯)
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
κ η : Kernel α γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
hκη : κ ≤ η
a : α
x : γ
⊢ 0 ≤ κ.rnDerivAux η a x

Tactic:
rw [rnDerivAux]
  split_ifs with hα
  · exact ENNReal.toReal_nonneg
  · have := hαγ.countableOrCountablyGenerated.resolve_left hα
    exact density_nonneg ((fst_map_id_prod _ measurable_const).trans_le hκη) _ _ _

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 = 0 ↔ κ a ≪ η a

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η, add_apply]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (κ.singularPart η) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (κ.singularPart η) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ≪ η a

Tactic:
h,

Goal state after:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (κ.singularPart η) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + 0 ≪ η a
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 : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ κ a ⟂ₘ η a

Tactic:
conv_rhs => rw [← rnDeriv_add_singularPart κ η, add_apply]

Goal state after:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ (η.withDensity (κ.rnDeriv η)) a = 0 ↔ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a
Module: Mathlib.Probability.Kernel.RadonNikodym

Goal state before:
pp: case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ (η.withDensity (κ.rnDeriv η)) a + (κ.singularPart η) a ⟂ₘ η a

Tactic:
h,

Goal state after:
case refine_1
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
h : (η.withDensity (κ.rnDeriv η)) a = 0
⊢ 0 + (κ.singularPart η) a ⟂ₘ η a
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
⊢ κ a = ξ a + (η a).withDensity (f a)

Tactic:
h,

Goal state after:
α : 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
⊢ (η.withDensity f + ξ) a = ξ a + (η a).withDensity (f a)
Module: Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj

Goal state before:
pp: case inr.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hbc✝ : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ ∫⁻ (z : (i : ↥(Iic b)) → X ↑i),
      ∫⁻ (z : (i : ↥(Iic c)) → X ↑i),
        f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ b c) z ∂(partialTraj κ a b) ((Iic a).restrict x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X ↑i), f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ a c) ((Iic a).restrict x₀)

Tactic:
← lintegral_comp,

Goal state after:
case inr.inr
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hbc✝ : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ ∫⁻ (c_1 : (i : ↥(Iic c)) → X ↑i),
      f (updateFinset x₀ (Iic c) c_1) ∂(partialTraj κ b c ∘ₖ partialTraj κ a b) ((Iic a).restrict x₀) =
    ∫⁻ (z : (i : ↥(Iic c)) → X ↑i), f (updateFinset x₀ (Iic c) z) ∂(partialTraj κ a c) ((Iic a).restrict x₀)

case inr.inr.hg
X : ℕ → Type u_1
mX : (n : ℕ) → MeasurableSpace (X n)
a b c : ℕ
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
hab✝ : a ≤ b
hbc✝ : b ≤ c
f : ((n : ℕ) → X n) → ℝ≥0∞
hf : Measurable f
x₀ : (n : ℕ) → X n
hab : a < b
hbc : b < c
⊢ Measurable fun z ↦ f (updateFinset x₀ (Iic c) z)
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 Ω
η : Kernel 𝓧 Ω
inst✝ : IsFiniteKernel η
h : (⇑κ ∘ₘ μ) ⊗ₘ η = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ
⊢ (⇑κ ∘ₘ μ) ⊗ₘ η = Measure.map Prod.swap (μ ⊗ₘ κ)

Tactic:
h,

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁴ : IsFiniteMeasure μ
inst✝³ : IsFiniteKernel κ
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
η : Kernel 𝓧 Ω
inst✝ : IsFiniteKernel η
h : (⇑κ ∘ₘ μ) ⊗ₘ η = ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ
⊢ ⇑(Kernel.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ = Measure.map Prod.swap (μ ⊗ₘ κ)
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)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
⊢ ∀ ⦃n_1 : ℕ⦄, n ≤ n_1 → Measure.map (frestrictLe n_1) (η x) = inducedFamily (fun n ↦ (partialTraj κ a n) x) (Iic n_1)

Tactic:
intro k

Goal state after:
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a n : ℕ
η : Kernel ((i : ↥(Iic a)) → X ↑i) ((n : ℕ) → X n)
hη : ∀ b ≥ n, η.map (frestrictLe b) = partialTraj κ a b
x : (i : ↥(Iic a)) → X ↑i
k : ℕ
⊢ n ≤ k → Measure.map (frestrictLe k) (η x) = inducedFamily (fun n ↦ (partialTraj κ a n) x) (Iic k)
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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ,
    (fun y ↦ ∫⁻ (x : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) (x, y).2 (x, y).1 ∂μ) x = (fun a ↦ ((κ†μ) a) s) x

Tactic:
filter_upwards [absolutelyContinuous_posterior h_ac] with x h_ac'

Goal state after:
Ω : 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 : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ
s : Set Ω
t : Set 𝓧
hs : MeasurableSet s
ht : MeasurableSet t
x : 𝓧
h_ac' : (κ†μ) x ≪ μ
⊢ ∫⁻ (x_1 : Ω) in s, (κ†μ).rnDeriv (Kernel.const 𝓧 μ) x x_1 ∂μ = ((κ†μ) x) s
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫⁻ (x : ℝ), betaPDF α β x = 1

Tactic:
lintegral_betaPDF,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫⁻ (x : ℝ) in Ioo 0 1, ENNReal.ofReal (1 / beta α β * x ^ (α - 1) * (1 - x) ^ (β - 1)) = 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]
  · simp [NNReal.smul_def]
  all_goals exact (integrable_dirac (by simp)).smul_measure_nnreal

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

Goal state before:
pp: a r x : ℝ
hx : x < 0
⊢ gammaPDF a r x = 0

Tactic:
by
  simp only [gammaPDF_eq, if_neg (not_le.mpr hx), ENNReal.ofReal_zero]

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ p.toOuterMeasure s = 0 ↔ Disjoint p.support s

Tactic:
toOuterMeasure_apply,

Goal state after:
α : Type u_1
p : PMF α
s : Set α
⊢ ∑' (x : α), s.indicator (⇑p) x = 0 ↔ Disjoint p.support s
Module: Mathlib.Probability.Distributions.Geometric

Goal state before:
pp: p : ↑unitInterval
h1 : p ≠ 0
h2 : p ≠ 1
n : ℕ
⊢ 0 < (geometricMeasure p).real {n}

Tactic:
rw [geometricMeasure_real_singleton h1]
  exact geometricMeasure_pos h1 h2 n

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

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ map s.restrict (map (fun ω i ↦ X i ω) P) = Measure.pi fun i ↦ map (s.restrict X i) P

pp: case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

pp: case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P

Tactic:
h,

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ map s.restrict (infinitePi fun i ↦ map (X i) P) = Measure.pi fun i ↦ map (s.restrict X i) P

case hg
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable s.restrict (map (fun ω i ↦ X i ω) P)

case hf
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
𝓧 : ι → Type u_3
m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)
X : (i : ι) → Ω → 𝓧 i
inst✝ : IsProbabilityMeasure P
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
this : (s.restrict ∘ fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω
⊢ AEMeasurable (fun ω i ↦ X i ω) P
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: α : 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
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ i, ⨆ (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
this : Nonempty (∃ i, n ∈ ns i)
⊢ ⨆ i, ⨆ (_ : n ∈ ns i), s n = s n

Tactic:
h,

Goal state after:
α : 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
h_indep : iIndep s κ μα
hf : ∀ (t : Set ι), p t → tᶜ ∈ f
hns : Directed (fun x1 x2 ↦ x1 ⊆ x2) ns
hnsp : ∀ (a : β), p (ns a)
hns_univ : ∀ (n : ι), ∃ a, n ∈ ns a
n : ι
h : ⨆ i, ⨆ (_ : n ∈ ns i), s n = ⨆ (_ : ∃ i, n ∈ ns i), s n
this : Nonempty (∃ i, n ∈ ns i)
⊢ ⨆ (_ : ∃ i, n ∈ ns i), s n = s n
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h✝ : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']
hf : ∀ i ∈ s, f i ∈ π i
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω
h : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω = (∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ω
h_ne_top : ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) ≠ ∞
this : ∏ i ∈ s, ((condExpKernel μ m') ω) (f i) ≠ ∞
⊢ ENNReal.ofReal (μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)

Tactic:
h,

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
h_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ᵐ (ω : Ω) ∂μ, ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq✝ :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      (fun ω ↦ (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal) =ᵐ[μ] μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
h✝ : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']
hf : ∀ i ∈ s, f i ∈ π i
ω : Ω
h_eq : ∀ i ∈ s, (((condExpKernel μ m') ω) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] ω
h_inter_eq : (((condExpKernel μ m') ω) (⋂ i ∈ s, f i)).toReal = μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω
h : μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] ω = (∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ω
h_ne_top : ((condExpKernel μ m') ω) (⋂ i ∈ s, f i) ≠ ∞
this : ∏ i ∈ s, ((condExpKernel μ m') ω) (f i) ≠ ∞
⊢ ENNReal.ofReal ((∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ω) = ∏ i ∈ s, ((condExpKernel μ m') ω) (f i)