mathlib-initiative/mathlib-tactics huggingface dataset:
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 : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ (trajFun κ a x₀) Set.univ = 1

Tactic:
rw [← cylinder_univ (Iic 0), trajFun, AddContent.measure_eq, trajContent_cylinder .univ,
      measure_univ]

Goal state after:
case hC_gen
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ MeasurableSpace.pi = generateFrom (measurableCylinders X)

case hs
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a : ℕ
x₀ : (i : ↥(Iic a)) → X ↑i
⊢ cylinder (Iic 0) Set.univ ∈ measurableCylinders X
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.swap Ω 𝓧) ∘ₘ μ ⊗ₘ κ

Tactic:
rw [compProd_posterior_eq_swap_comp]

Goal state after:
Module: Mathlib.Probability.ProductMeasure

Goal state before:
pp: case ha.hs
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
⊢ ∀ (i : Finset ↑s), NullMeasurableSet ((Subtype.val '' ↑i).pi fun i ↦ if i ∈ s then t i else Set.univ) (infinitePi μ)

Tactic:
refine fun s' ↦ MeasurableSet.nullMeasurableSet (MeasurableSet.pi ?_ (by measurability))

Goal state after:
case ha.hs
ι✝ : Type u_1
X✝ : ι✝ → Type u_2
mX✝ : (i : ι✝) → MeasurableSpace (X✝ i)
μ✝ : (i : ι✝) → Measure (X✝ i)
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
s : Set ι
hs : Countable ↑s
t : (i : ι) → Set (X i)
mt : ∀ i ∈ s, MeasurableSet (t i)
s_ne : Nonempty ↑s
this : s.pi t = ⋂ s', (Subtype.val '' ↑s').pi fun i ↦ if i ∈ s then t i else Set.univ
s' : Finset ↑s
⊢ (Subtype.val '' ↑s').Countable
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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
⊢ μ ⊗ₘ κ ≪ μ.prod (⇑κ ∘ₘ μ)

Tactic:
rw [← swap_compProd_posterior, ← Measure.prod_swap, Measure.swap_comp]

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 : ∀ᵐ (b : 𝓧) ∂⇑κ ∘ₘ μ, (κ†μ) b ≪ μ
this : (⇑κ ∘ₘ μ) ⊗ₘ κ†μ ≪ (⇑κ ∘ₘ μ).prod μ
⊢ Measure.map Prod.swap ((⇑κ ∘ₘ μ) ⊗ₘ κ†μ) ≪ Measure.map Prod.swap ((⇑κ ∘ₘ μ).prod μ)
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 Ω 𝓧
ν : Measure 𝓧
inst✝ : SFinite ν
h_ac : ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ν
⊢ ∀ᵐ (ω : Ω) ∂μ, κ ω ≪ ⇑κ ∘ₘ μ

Tactic:
by
  rw [← absolutelyContinuous_posterior_iff]
  exact absolutelyContinuous_posterior 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 : ↥s) → X ↑i), g y ∂Measure.pi fun i ↦ μ ↑i) = (∫⋯∫⁻_s, f ∂μ) x

pp: case hf
ι : 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
⊢ Measurable g

Tactic:
· rfl

Goal state after:
case hf
ι : 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
⊢ Measurable g
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 Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ ∑' (i : 𝓨), ∫⁻ (a : Θ), ℓ a i * ((κ ∘ₖ P) a) {i} ∂π = ∑' (y : 𝓨), ∫⁻ (θ : Θ), ℓ θ y * (⇑κ ∘ₘ P θ) {y} ∂π

pp: Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ ∀ (i : 𝓨), AEMeasurable (fun θ ↦ ℓ θ i * ((κ ∘ₖ P) θ) {i}) π

Tactic:
· rfl

Goal state after:
Θ : Type u_1
𝓧 : Type u_3
𝓨 : Type u_5
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
κ : Kernel 𝓧 𝓨
π : Measure Θ
inst✝¹ : Countable 𝓨
inst✝ : MeasurableSingletonClass 𝓨
hℓ : Measurable ℓ
⊢ ∀ (i : 𝓨), AEMeasurable (fun θ ↦ ℓ θ i * ((κ ∘ₖ P) θ) {i}) π
Module: Mathlib.Probability.Decision.BayesEstimator

Goal state before:
pp: Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hl : Measurable (Function.uncurry ℓ)
h : HasArgminEstimator ℓ P π
⊢ avgRisk ℓ P ⋯.kernel π = ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π

Tactic:
h.isArgminEstimator_argminEstimator.avgRisk_eq_lintegral_iInf hl

Goal state after:
Θ : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
mΘ : MeasurableSpace Θ
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
ℓ : Θ → 𝓨 → ℝ≥0∞
P : Kernel Θ 𝓧
π : Measure Θ
inst✝³ : StandardBorelSpace Θ
inst✝² : Nonempty Θ
inst✝¹ : IsFiniteKernel P
inst✝ : IsFiniteMeasure π
hl : Measurable (Function.uncurry ℓ)
h : HasArgminEstimator ℓ P π
⊢ ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π = ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(P†π) x ∂⇑P ∘ₘ π
Module: Mathlib.Probability.Distributions.Beta

Goal state before:
pp: α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (a : ℝ) in Ioo 0 1, a ^ (α - 1) * (1 - a) ^ (β - 1) =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1) ∂volume).re

Tactic:
← integral_Ioc_eq_integral_Ioo,

Goal state after:
α β : ℝ
hα : 0 < α
hβ : 0 < β
⊢ ∫ (t : ℝ) in Ioc 0 1, t ^ (α - 1) * (1 - t) ^ (β - 1) =
    (∫ (x : ℝ) in Ioc 0 1, ↑x ^ (↑α - 1) * (1 - ↑x) ^ (↑β - 1) ∂volume).re
Module: Mathlib.Probability.Distributions.Binomial

Goal state before:
pp: R : Type u_1
inst✝³ : MeasurableSpace R
inst✝² : AddMonoidWithOne R
n : ℕ
p : ↑I
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : MeasurableSingletonClass R
f : R → E
⊢ Integrable f Bin(R, n, p)

Tactic:
by
  simp [map_cast_binomial_eq_sum_dirac, integrable_finsetSum_measure, integrable_dirac,
    Integrable.smul_measure]

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

Goal state before:
pp: case pos
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X ↑i
y : (n : ℕ) → X n
hx : x ∈ A
⊢ uncurry (fun x y ↦ A.indicator (fun x ↦ f x y) x) (x, y) = (A ×ˢ Set.univ).indicator (uncurry f) (x, y)

Tactic:
simp [uncurry_def, hx]

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

Goal state before:
pp: case neg
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
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
f : ((i : ↥(Iic b)) → X ↑i) → ((n : ℕ) → X n) → E
hf : Integrable (uncurry f) ((partialTraj κ a b) u ⊗ₘ traj κ b)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
x : (i : ↥(Iic b)) → X ↑i
y : (n : ℕ) → X n
hx : x ∉ A
⊢ uncurry (fun x y ↦ A.indicator (fun x ↦ f x y) x) (x, y) = (A ×ˢ Set.univ).indicator (uncurry f) (x, y)

Tactic:
simp [uncurry_def, hx]

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

Goal state before:
pp: α : Type u_1
p : PMF α
s : Set α
⊢ (∀ (i : α), s.indicator (⇑p) i = 0) ↔ Disjoint p.support s

Tactic:
exact funext_iff.symm.trans Set.indicator_eq_zero'

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

Goal state before:
pp: p : ℝ
n : ℕ
hp_pos : 0 < p
hp_lt_one : p < 1
⊢ 0 < (1 - p) ^ n * p

Tactic:
positivity [sub_pos.mpr hp_lt_one]

Goal state after:
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
mR : MeasurableSpace R
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝ : MeasurableAdd₂ R
r₁ r₂ : ℝ≥0
X Y : Ω → R
hXY : X ⟂ᵢ[P] Y
hX : HasLaw X Po(R, r₁) P
hY : HasLaw Y Po(R, r₂) P
⊢ HasLaw (X + Y) Po(R, r₁ + r₂) P

Tactic:
by
  rw [← map_cast_poissonMeasure_conv]
  exact hXY.hasLaw_add hX hY

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ (uniformOfFinset s hs) a = (↑(#s))⁻¹

Tactic:
by
  simp [ha]

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
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ iIndepFun X P

Tactic:
iIndepFun_iff_map_fun_eq_infinitePi_map₀ hm,

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
μ : (i : ι) → Measure (𝓧 i)
hX : ∀ (i : ι), HasLaw (X i) (μ i) P
hm : AEMeasurable (fun ω i ↦ X i ω) P
h : HasLaw (fun ω i ↦ X i ω) (infinitePi μ) P
⊢ map (fun ω i ↦ X i ω) P = infinitePi fun i ↦ map (X i) P
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, f i ∈ {s | MeasurableSet s}) →
        μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']) ↔
    ∀ (s : Finset ι) {f : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (f i)) →
        μ[(⋂ i ∈ s, f i).indicator fun ω ↦ 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(f i).indicator fun ω ↦ 1 | m']

pp: case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
· rfl

Goal state after:
case hπ
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
m : ι → MeasurableSpace Ω
hm : ∀ (i : ι), m i ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ (∀ (t1 t2 : Set Ω),
      t1 ∈ {s | MeasurableSet s} →
        t2 ∈ {s | MeasurableSet s} →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']) ↔
    ∀ (t1 t2 : Set Ω),
      MeasurableSet t1 →
        MeasurableSet t2 →
          μ[(t1 ∩ t2).indicator fun ω ↦ 1 | m'] =ᵐ[μ] μ[t1.indicator fun ω ↦ 1 | m'] * μ[t2.indicator fun ω ↦ 1 | m']

pp: case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

pp: case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

Tactic:
· rfl

Goal state after:
case hs1
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s

case hs2
Ω : Type u_1
m' m₁ m₂ mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
hm₁ : m₁ ≤ mΩ
hm₂ : m₂ ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ s ∈ {s | MeasurableSet s}, MeasurableSet s
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
⊢ (μ.tilted fun x ↦ t * X x) s = ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ

Tactic:
by
  rw [tilted_apply, mgf]

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

Goal state before:
pp: p : ℝ≥0
h : p ≤ 1
n : ℕ
⊢ (binomial p h n) (Fin.last n) = ↑p ^ n

Tactic:
by simp [binomial_apply_last]

Goal state after:
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF id c (κ.map X) ν
⊢ HasSubgaussianMGF X c κ ν

pp: case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)

pp: case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
· change HasSubgaussianMGF (id ∘ X) c κ ν
    exact .of_map hX h

Goal state after:
case refine_2
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
t : ℝ
⊢ Integrable (fun ω ↦ rexp (t * id ω)) (⇑(κ.map X) ∘ₘ ν)

case refine_3
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
hX : Measurable X
h : HasSubgaussianMGF X c κ ν
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf id ((κ.map X) ω') t ≤ rexp (↑c * t ^ 2 / 2)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : (fun x ↦ σ n x ω) (nk n) ≤ (fun x ↦ σ n x ω) (mkStrictMonoAux nk n)
⊢ {ω | σ n (mkStrictMonoAux nk n) ω < min (τ n ω) ↑(T n)} ω ≤ {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ω

Tactic:
simp [Set.ofPred]

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
nk : ℕ → ℕ
hnk : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
n : ℕ
ω : Ω
hω : (fun x ↦ σ n x ω) (nk n) ≤ (fun x ↦ σ n x ω) (mkStrictMonoAux nk n)
⊢ σ n (mkStrictMonoAux nk n) ω < τ n ω →
    σ n (mkStrictMonoAux nk n) ω < ↑(T n) → σ n (nk n) ω < τ n ω ∧ σ n (nk n) ω < ↑(T n)
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
⊢ ∃ nk, StrictMono nk ∧ IsPreLocalizingSequence 𝓕 (fun i ω ↦ min (τ i ω) (σ i (nk i) ω)) P

Tactic:
obtain ⟨nk, T, hnk, hT, hP⟩ := isPreLocalizingSequence_of_isLocalizingSequence_aux hτ hσ
  refine ⟨nk, hnk, fun n ↦ (hτ.isStoppingTime n).min ((hσ _).isStoppingTime _), ?_⟩
  have : ∑' n, P {ω | σ n (nk n) ω < min (τ n ω) (T n)} < ∞ :=
    lt_of_le_of_lt (ENNReal.summable.tsum_mono ENNReal.summable hP)
      (tsum_geometric_lt_top.2 <| by simp)
  filter_upwards [ae_eventually_notMem this.ne, hτ.tendsto_top] with ω hω hωτ
  exact hωτ.min <| tendsto_of_tendsto_of_tendsto_of_le_of_le'
    (hωτ.min <| WithTop.tendsto_coe_atTop.comp hT) tendsto_const_nhds (by grind) (by simp)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
⊢ Monotone fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}

Tactic:
intro m n hmn x hx

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K i : ℕ
x✝ : i ∈ range K
this : {ω | X ω ∈ Set.Ioi ↑i} = ⋃ N, {ω | X ω ∈ Set.Ioc ↑i ↑N}
m n : ℕ
hmn : m ≤ n
x : Ω
hx : x ∈ (fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}) m
⊢ x ∈ (fun N ↦ {ω | X ω ∈ Set.Ioc ↑i ↑N}) n
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ cgf X μ t ≤ ↑c * t ^ 2 / 2

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using (all_ae_of h.cgf_le t)

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
⊢ ∀ᵐ (ω : Ω),
    (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊

Tactic:
filter_upwards [strong_law_aux2 X hint hindep hident hnonneg c_one] with ω hω

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ω : Ω
hω :
  (fun n ↦
      ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω -
        ∫ (a : Ω), (∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) ↑i) a) =o[atTop]
    fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ average k G * single g 1 = average k G

Tactic:
simp only [mul_one, Finset.sum_mul, Algebra.smul_mul_assoc, average, MonoidAlgebra.of_apply,
    MonoidAlgebra.single_mul_single]

Goal state after:
k : Type u_1
G : Type u_2
inst✝³ : CommSemiring k
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
g : G
⊢ ⅟↑(Fintype.card G) • ∑ x, single (x * g) 1 = ⅟↑(Fintype.card G) • ∑ x, single x 1
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
x✝¹ : res φ (leftRegular k H) ⟶ A
x✝ : H
⊢ ((Hom.hom
            ({
                toFun := fun f ↦
                  (resFunctor φ).map (↑(leftRegular k H).leftRegularHomEquiv.symm (MonoidAlgebra.single 1 1)) ≫ f,
                map_add' := ⋯, map_smul' := ⋯ }
              x✝¹)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((Hom.hom (1 x✝¹)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
simp [homEquiv]

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u
G : Type v
H : Type w
inst✝² : CommRing k
inst✝¹ : Monoid G
inst✝ : Monoid H
φ : G →* H
A : Rep k G
h : H
x✝ : ↥(Representation.coindV φ A.ρ)
h✝ : H
⊢ (Hom.hom ((↑(coindVEquiv φ A) ∘ₗ (Representation.coind φ A.ρ) h) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1) =
    (Hom.hom (((Representation.coind' φ A) h ∘ₗ ↑(coindVEquiv φ A)) x✝)).toLinearMap (MonoidAlgebra.single h✝ 1)

Tactic:
simp [homEquiv]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (lTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (lid k Y✝.ρ)).hom)).toLinearMap)
        1)
      x✝ =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (lid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) 1) x✝

Tactic:
simp [trivial_V]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
X✝ Y✝ : Rep k G
x✝¹ : X✝ ⟶ Y✝
x✝ : ↑X✝
⊢ ((TensorProduct.AlgebraTensorModule.curry
          (Hom.hom (ofHom (rTensor (trivial k G k).ρ (Hom.hom x✝¹)) ≫ (mkIso (rid k Y✝.ρ)).hom)).toLinearMap)
        x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry (Hom.hom ((mkIso (rid k X✝.ρ)).hom ≫ x✝¹)).toLinearMap) x✝) 1

Tactic:
simp [trivial_V]

Goal state after:
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : CommRing k
inst✝ : Monoid G
A : Rep k G
x : ↑A
g : G
⊢ (Hom.hom (A.leftRegularHomEquiv.symm x)) (MonoidAlgebra.single g 1) = (A.ρ g) x

Tactic:
simp [homEquiv]

Goal state after: