mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ cexp ((∫ (x : E), ↑((L ∘SL inl ℝ E F) x) ∂Measure.map X P) * I - ↑Var[⇑(L ∘SL inl ℝ E F); Measure.map X P] / 2) =
    cexp
      (↑(L ((inl ℝ E F) (∫ (x : E), x ∂Measure.map X P))) * I -
        ↑(((covarianceBilinDual (Measure.map X P)) (L ∘SL inl ℝ E F)) (L ∘SL inl ℝ E F)) / 2)

Tactic:
integral_complex_ofReal,

Goal state after:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ cexp (↑(∫ (x : E), (L ∘SL inl ℝ E F) x ∂Measure.map X P) * I - ↑Var[⇑(L ∘SL inl ℝ E F); Measure.map X P] / 2) =
    cexp
      (↑(L ((inl ℝ E F) (∫ (x : E), x ∂Measure.map X P))) * I -
        ↑(((covarianceBilinDual (Measure.map X P)) (L ∘SL inl ℝ E F)) (L ∘SL inl ℝ E F)) / 2)
Module: Mathlib.Probability.Distributions.Gaussian.HasGaussianLaw.Independence

Goal state before:
pp: case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ cexp ((∫ (x : F), ↑((L ∘SL inr ℝ E F) x) ∂Measure.map Y P) * I - ↑Var[⇑(L ∘SL inr ℝ E F); Measure.map Y P] / 2) =
    cexp
      (↑(L ((inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P))) * I -
        ↑(((covarianceBilinDual (Measure.map Y P)) (L ∘SL inr ℝ E F)) (L ∘SL inr ℝ E F)) / 2)

Tactic:
integral_complex_ofReal,

Goal state after:
case e_a
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
E : Type u_2
F : Type u_3
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : MeasurableSpace E
inst✝⁹ : CompleteSpace E
inst✝⁸ : BorelSpace E
inst✝⁷ : SecondCountableTopology E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : MeasurableSpace F
inst✝⁴ : CompleteSpace F
inst✝³ : BorelSpace F
inst✝² : SecondCountableTopology F
inst✝¹ : NormedSpace ℝ E
inst✝ : NormedSpace ℝ F
X : Ω → E
Y : Ω → F
hX : HasGaussianLaw X P
hY : HasGaussianLaw Y P
hXY : X ⟂ᵢ[P] Y
this✝ : IsProbabilityMeasure P
L : StrongDual ℝ (E × F)
this :
  (∫ (x : E), x ∂Measure.map X P, ∫ (y : F), y ∂Measure.map Y P) =
    (inl ℝ E F) (∫ (x : E), x ∂Measure.map X P) + (inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P)
⊢ cexp (↑(∫ (x : F), (L ∘SL inr ℝ E F) x ∂Measure.map Y P) * I - ↑Var[⇑(L ∘SL inr ℝ E F); Measure.map Y P] / 2) =
    cexp
      (↑(L ((inr ℝ E F) (∫ (y : F), y ∂Measure.map Y P))) * I -
        ↑(((covarianceBilinDual (Measure.map Y P)) (L ∘SL inr ℝ E F)) (L ∘SL inr ℝ E F)) / 2)
Module: Mathlib.Probability.Kernel.Disintegration.Basic

Goal state before:
pp: case pos.left
α : 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
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0

Tactic:
let s := {b | r ≤ κCond (a, b) Set.univ}

Goal state after:
case pos.left
α : 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
h_meas : Measurable fun b ↦ (κCond (a, b)) univ
r : ℝ≥0∞
hr : 1 < r
s : Set β := {b | r ≤ (κCond (a, b)) univ}
⊢ (κ.fst a) {x | r ≤ (κCond (a, x)) univ} = 0
Module: Mathlib.Probability.Kernel.Disintegration.Density

Goal state before:
pp: case 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 ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ Integrable (fun x ↦ κ.densityProcess ν j a x s) (ν a)

pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ), MeasurableSet s_1 → (ν a) s_1 < ∞ → IntegrableOn (fun x ↦ κ.densityProcess ν i a x s) s_1 (ν a)

pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      (ν a) s_1 < ∞ →
        ∫ (x : γ) in s_1, κ.densityProcess ν i a x s ∂ν a = ∫ (x : γ) in s_1, κ.densityProcess ν j a x s ∂ν a

pp: case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun x ↦ κ.densityProcess ν i a x s) (ν a)

Tactic:
· exact integrable_densityProcess hκν j a hs

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ), MeasurableSet s_1 → (ν a) s_1 < ∞ → IntegrableOn (fun x ↦ κ.densityProcess ν i a x s) s_1 (ν a)

case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ ∀ (s_1 : Set γ),
    MeasurableSet s_1 →
      (ν a) s_1 < ∞ →
        ∫ (x : γ) in s_1, κ.densityProcess ν i a x s ∂ν a = ∫ (x : γ) in s_1, κ.densityProcess ν j a x s ∂ν a

case refine_4
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
i j : ℕ
hij : i ≤ j
a : α
s : Set β
hs : MeasurableSet s
⊢ AEStronglyMeasurable (fun x ↦ κ.densityProcess ν i a x s) (ν a)
Module: Mathlib.Probability.Kernel.Disintegration.Integral

Goal state before:
pp: β : Type u_1
Ω : Type u_2
mβ : MeasurableSpace β
inst✝³ : MeasurableSpace Ω
inst✝² : StandardBorelSpace Ω
inst✝¹ : Nonempty Ω
ρ : Measure (β × Ω)
inst✝ : IsFiniteMeasure ρ
s : Set (β × Ω)
hs : MeasurableSet s
⊢ ∫⁻ (x : β), (ρ.condKernel x) {y | (x, y) ∈ s} ∂ρ.fst = ρ s

Tactic:
by
  conv_rhs => rw [← ρ.disintegrate ρ.condKernel]
  simp_rw [compProd_apply hs]
  rfl

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map : ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑(condDistrib (Y ∘ Prod.fst) (X ∘ Prod.fst) (μ.prod ν))
⊢ ⇑(condDistrib (fun ω ↦ Y ω.1) (fun ω ↦ X ω.1) (μ.prod ν)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
exact h_map.symm

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

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
Ω : Type u_3
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
mα : MeasurableSpace α
μ : Measure α
inst✝¹ : IsFiniteMeasure μ
Y : α → Ω
mβ : MeasurableSpace β
γ : Type u_5
mγ : MeasurableSpace γ
X : α → β
hY : AEMeasurable Y μ
ν : Measure γ
inst✝ : IsProbabilityMeasure ν
hX : AEMeasurable X μ
h_map : ⇑(condDistrib Y X μ) =ᵐ[Measure.map X μ] ⇑(condDistrib (Y ∘ Prod.snd) (X ∘ Prod.snd) (ν.prod μ))
⊢ ⇑(condDistrib (fun ω ↦ Y ω.2) (fun ω ↦ X ω.2) (ν.prod μ)) =ᵐ[Measure.map X μ] ⇑(condDistrib Y X μ)

Tactic:
exact h_map.symm

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

Goal state before:
pp: ι : Type u_1
s : Set ι
p : ↑I
inst✝ : Countable ι
u : Finset ι
hsu : s ⊆ ↑u
⊢ ∏' (i : ι), ((if i ∈ u ↔ i ∈ s then ↑(toNNReal p) else 0) + if i ∈ s then 0 else ↑(toNNReal (σ p))) =
    ∏ i ∈ u, if i ∈ s then ↑(toNNReal p) else ↑(toNNReal (σ p))

Tactic:
rw [tprod_eq_prod, Finset.prod_congr rfl] <;>
        simp +contextual [ite_add_ite, mt (@hsu _), ← ENNReal.coe_add]

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 J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ (Measure.map (restrict₂ hJI) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I)) (Set.univ.pi s) = ∏ i, (μ ↑i) (s i)

Tactic:
simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ ∏ x ∈ I, Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x =
    ∏ x ∈ J, Function.extend Subtype.val (fun i ↦ (μ ↑i) (s i)) 1 x
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) =
    Function.extend Subtype.val (fun i ↦ (μ ↑i) (if h : ↑i ∈ J then s ⟨↑i, h⟩ else Set.univ)) 1 x

Tactic:
Function.extend_val_apply (hJI hx),

Goal state after:
case refine_2
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
I J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
x : ι
hx : x ∈ J
⊢ (μ ↑⟨x, hx⟩) (s ⟨x, hx⟩) = (μ ↑⟨x, ⋯⟩) (if h : ↑⟨x, ⋯⟩ ∈ J then s ⟨↑⟨x, ⋯⟩, h⟩ else Set.univ)
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 J : Finset ι
hJI : J ⊆ I
s : (i : ↥J) → Set (X ↑i)
ms : ∀ (i : ↥J), MeasurableSet (s i)
⊢ (Measure.map (restrict₂ hJI) ((fun I ↦ Measure.pi fun i ↦ μ ↑i) I)) (Set.univ.pi s) = ∏ i, (μ ↑i) (s i)

Tactic:
simp_rw [Measure.map_apply (measurable_restrict₂ hJI) (.univ_pi ms), restrict₂_preimage hJI,
    Measure.pi_pi, prod_eq_prod_extend]
  refine (prod_subset_one_on_sdiff hJI (fun x hx ↦ ?_) (fun x hx ↦ ?_)).symm
  · rw [Function.extend_val_apply (mem_sdiff.1 hx).1, dif_neg (mem_sdiff.1 hx).2, measure_univ]
  · rw [Function.extend_val_apply hx, Function.extend_val_apply (hJI hx), dif_pos hx]

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 Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝ : IsEmpty 𝓨
⊢ avgRisk ℓ P κ π = 0

Tactic:
by
  simp [Subsingleton.elim κ 0]

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✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
h_eq_sum : κ.withDensity f = Kernel.sum fun i ↦ (κ.seq i).withDensity f
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
h_eq_sum

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
h_eq_sum : κ.withDensity f = Kernel.sum fun i ↦ (κ.seq i).withDensity f
⊢ IsSFiniteKernel (Kernel.sum fun i ↦ (κ.seq i).withDensity f)
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)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)

Tactic:
let aux n : t n ≃ s n :=
    { toFun := fun i ↦ ⟨i.1.1, mem_preimage.1 i.2⟩
      invFun := fun i ↦ ⟨⟨i.1, Set.mem_iUnion.2 ⟨n, i.2⟩⟩, mem_preimage.2 i.2⟩
      left_inv := fun i ↦ by simp
      right_inv := fun i ↦ by simp }

Goal state after:
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
A : ℕ → Set ((i : ι) → X i)
A_mem : ∀ (n : ℕ), A n ∈ measurableCylinders X
A_anti : Antitone A
A_inter : ⋂ n, A n = ∅
this : ∀ (i : ι), Nonempty (X i)
s : ℕ → Finset ι
S : (n : ℕ) → Set ((i : ↥(s n)) → X ↑i)
mS : ∀ (n : ℕ), MeasurableSet (S n)
A_eq : ∀ (n : ℕ), A n = cylinder (s n) (S n)
u : Set ι := ⋃ n, ↑(s n)
t : ℕ → Finset ↑u := fun n ↦ (s n).preimage Subtype.val ⋯
f : ((i : ↑u) → X ↑i) → (i : ι) → X i := fun x i ↦ if hi : i ∈ u then x ⟨i, hi⟩ else Classical.ofNonempty
aux : (n : ℕ) → ↥(t n) ≃ ↥(s n) :=
  fun n ↦ { toFun := fun i ↦ ⟨↑↑i, ⋯⟩, invFun := fun i ↦ ⟨⟨↑i, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }
⊢ Tendsto (fun n ↦ (piContent μ) (A n)) atTop (𝓝 0)
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: ι : Type u_6
κ : Type u_7
X : Type u_8
mX : MeasurableSpace X
μ : ι → κ → Measure X
hμ : ∀ (i : ι) (j : κ), IsProbabilityMeasure (μ i j)
⊢ map (⇑(MeasurableEquiv.curry ι κ X)) (infinitePi fun p ↦ μ p.1 p.2) = infinitePi fun i ↦ infinitePi fun j ↦ μ i j

Tactic:
by
  rw [MeasurableEquiv.map_apply_eq_iff_map_symm_apply_eq, infinitePi_map_curry_symm]

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

Goal state before:
pp: 𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv :
  ∀ (ω : Ω), κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω =ᵐ[(Kernel.const Ω (⇑κ ∘ₘ μ)) ω] ∂κ ω/∂(Kernel.const Ω (⇑κ ∘ₘ μ)) ω
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x

Tactic:
simp only [Filter.EventuallyEq, Kernel.const_apply] at h_rnDeriv

Goal state after:
𝓧 : Type u_2
m𝓧 : MeasurableSpace 𝓧
Ω : Type u_5
inst✝⁵ : Countable Ω
inst✝⁴ : MeasurableSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace Ω
κ : Kernel Ω 𝓧
inst✝¹ : IsFiniteKernel κ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_rnDeriv : ∀ (ω : Ω), ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, κ.rnDeriv (Kernel.const Ω (⇑κ ∘ₘ μ)) ω x = (∂κ ω/∂⇑κ ∘ₘ μ) x
⊢ ∀ᵐ (x : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) x = μ.withDensity fun ω ↦ (∂κ ω/∂⇑κ ∘ₘ μ) x
Module: Mathlib.Probability.Decision.Risk.Countable

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝¹ : Fintype Θ
inst✝ : MeasurableSingletonClass Θ
⊢ bayesRisk ℓ P π = ⨅ κ, ⨅ (_ : IsMarkovKernel κ), ∑ θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ ∘ₖ P) θ) * π {θ}

Tactic:
by
  simp [bayesRisk, avgRisk_fintype]

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝² : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝¹ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
hf : AEStronglyMeasurable f ((traj κ a) x₀)
⊢ ∀ᵐ (x : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, AEStronglyMeasurable f ((traj κ b) x)

Tactic:
← traj_comp_partialTraj hab

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)
E : Type u_2
inst✝ : NormedAddCommGroup E
a b : ℕ
hab : a ≤ b
f : ((n : ℕ) → X n) → E
x₀ : (i : ↥(Iic a)) → X ↑i
hf : AEStronglyMeasurable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ ∀ᵐ (x : (i : ↥(Iic b)) → X ↑i) ∂(partialTraj κ a b) x₀, AEStronglyMeasurable f ((traj κ b) x)
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: n : ℕ
p : ↑I
E : Type u_3
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℕ → E
⊢ ∫ (x : ℕ), f x ∂Bin(n, p) = ∑ k ≤ n, (↑(n.choose k) * ↑p ^ k * (1 - ↑p) ^ (n - k)) • f k

Tactic:
rw [binomial_eq_sum_dirac, integral_finsetSum_measure]
  · simp
  exact fun _ _ ↦ (integrable_dirac (by simp)).smul_measure (by simp)

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

Goal state before:
pp: X : ℕ → Type u_1
inst✝⁴ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝³ : ∀ (n : ℕ), IsMarkovKernel (κ n)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
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₀)
⊢ Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ((partialTraj κ a b) x₀)

Tactic:
← traj_comp_partialTraj hab

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)
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 κ b ∘ₖ partialTraj κ a b) x₀)
⊢ Integrable (fun x ↦ ∫ (y : (n : ℕ) → X n), f y ∂(traj κ b) x) ((partialTraj κ a b) x₀)
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
x : ℝ
this : IsProbabilityMeasure (gammaMeasure a r)
b : ℝ
⊢ 0 b ≤ gammaPDFReal a r b

Tactic:
simp [gammaPDFReal_nonneg ha hr]

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

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : Nonempty α
s : Set α
inst✝¹ : MeasurableSpace α
hs : MeasurableSet s
inst✝ : Fintype ↑s
⊢ (uniformOfFintype α).toMeasure s = ↑(Fintype.card ↑s) / ↑(Fintype.card α)

Tactic:
simp [uniformOfFintype, Fintype.card_subtype, hs]

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

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
t : Set α
⊢ (ofMultiset s hs).toOuterMeasure t = (∑' (x : α), ↑(Multiset.count x (Multiset.filter (fun x ↦ x ∈ t) s))) / ↑s.card

Tactic:
simp_rw [div_eq_mul_inv, ← ENNReal.tsum_mul_right, toOuterMeasure_apply]
  refine tsum_congr fun x => ?_
  by_cases hx : x ∈ t <;> simp [Set.indicator, hx, div_eq_mul_inv]

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

Goal state before:
pp: case neg.refine_2.inr.inr.inr
Ω : 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
⊢ μ.real s • (μ.real s)⁻¹ • ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ

Tactic:
smul_inv_smul₀

Goal state after:
case neg.refine_2.inr.inr.inr
Ω : 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
⊢ ∫ (x : Ω) in s, f x ∂μ = ∫ (x : Ω) in s, f x ∂μ

case neg.refine_2.inr.inr.inr.ha
Ω : 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
⊢ μ.real s ≠ 0
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ ((κ₁.hom ∥ₖ κ₂.hom ∥ₖ η.hom) a✝) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
rw [Kernel.parallelComp_apply]

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom ∥ₖ κ₂.hom) a✝.1).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom ∥ₖ κ₂.hom) a✝.1).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) = ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝

Tactic:
rw [Kernel.parallelComp_apply]

Goal state after:
X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
a✝ : (X₁✝.carrier × X₂✝.carrier) × X₃✝.carrier
s✝ : Set (Y₁✝.carrier × Y₂✝.carrier × Y₃✝.carrier)
hs : MeasurableSet s✝
⊢ (((κ₁.hom a✝.1.1).prod (κ₂.hom a✝.1.2)).prod (η.hom a✝.2)) (⇑prodAssoc ⁻¹' s✝) =
    ((κ₁.hom ∥ₖ (κ₂.hom ∥ₖ η.hom)) (prodAssoc a✝)) s✝