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

Goal state before:
pp: case inl
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : ↑n ≤ τ ω
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : τ ω < ↑n
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω

Tactic:
· rw [stoppedProcess_eq_of_le h, Set.indicator_of_mem, Finset.sum_eq_zero, add_zero]
    · intro m hm
      refine Set.indicator_of_notMem ?_ _
      rw [Finset.mem_filter] at hm
      simp only [Set.mem_ofPred_eq]
      refine (lt_of_lt_of_le ?_ h).ne'
      exact mod_cast hm.2
    · exact h

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
hbdd : ∀ (ω : Ω), τ ω < ↑n → τ ω ∈ WithTop.some '' ↑s
ω : Ω
h : τ ω < ↑n
⊢ stoppedProcess u τ n ω = {a | ↑n ≤ τ a}.indicator (u n) ω + ∑ c ∈ s with c < n, {ω | τ ω = ↑c}.indicator (u c) ω
Module: Mathlib.Probability.Distributions.Gaussian.Real

Goal state before:
pp: μ : ℝ
v : ℝ≥0
x y : ℝ
⊢ gaussianPDFReal μ v (x + y) = gaussianPDFReal (μ - y) v x

Tactic:
by
  rw [sub_eq_add_neg, ← gaussianPDFReal_sub, sub_eq_add_neg, neg_neg]

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

Goal state before:
pp: case e'_4.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

pp: case e'_4.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

pp: case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x ≠ 0

Tactic:
· nth_rw 2 [abs_of_nonneg]
      simp [hx.le]

Goal state after:
case e'_4.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x ≠ 0
Module: Mathlib.Probability.Moments.IntegrableExpMul

Goal state before:
pp: case e'_4.e'_6
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x = ||t| - x|

pp: case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x ≠ 0

Tactic:
· nth_rw 2 [abs_of_nonneg]
      simp [hx.le]

Goal state after:
case hbc
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t v x : ℝ
h_int_pos : Integrable (fun ω ↦ rexp ((v + t) * X ω)) μ
h_int_neg : Integrable (fun ω ↦ rexp ((v - t) * X ω)) μ
h_nonneg : 0 ≤ x
hx : x < |t|
p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hX : AEMeasurable X μ
a : Ω
this : |t| = |t| - x + x
⊢ |t| - x ≠ 0
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑u ^ 2 * ↑Var[⇑L; μ]

Tactic:
← ofReal_pow,

Goal state after:
case e_a.e_a
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : IsFiniteMeasure μ
h : ∀ (L : StrongDual ℝ E), charFunDual μ L = cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2)
L : StrongDual ℝ E
u : ℝ
⊢ ↑Var[⇑(u • L); μ] = ↑(u ^ 2) * ↑Var[⇑L; μ]
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L x) ∂Measure.map (fun x ↦ x + c) μ) * I - ↑Var[⇑L; Measure.map (fun x ↦ x + c) μ] / 2)

Tactic:
variance_map (by fun_prop) (by fun_prop),

Goal state after:
E : Type u_1
F : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace ℝ E
inst✝⁶ : MeasurableSpace E
inst✝⁵ : BorelSpace E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : MeasurableSpace F
inst✝¹ : BorelSpace F
μ : Measure E
inst✝ : IsGaussian μ
c : E
L : StrongDual ℝ E
hL_comp : (⇑L ∘ fun x ↦ x + c) = fun x ↦ L x + L c
⊢ cexp ((∫ (x : E), ↑(L x) ∂μ) * I - ↑Var[⇑L; μ] / 2 + ↑(L c) * I) =
    cexp ((∫ (x : E), ↑(L x) ∂Measure.map (fun x ↦ x + c) μ) * I - ↑Var[⇑L ∘ fun x ↦ x + c; μ] / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Basic

Goal state before:
pp: case e_a.e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ∫ (x : E), ↑(L₁ x) ∂μ + ∫ (x : F), ↑(L₂ x) ∂ν = ∫ (x : E × F), ↑(L x) ∂μ.prod ν

Tactic:
simp_rw [integral_complex_ofReal]

Goal state after:
case e_a.e_a
E : Type u_1
F : Type u_2
inst✝¹⁰ : NormedAddCommGroup E
inst✝⁹ : NormedSpace ℝ E
inst✝⁸ : MeasurableSpace E
inst✝⁷ : BorelSpace E
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace ℝ F
inst✝⁴ : MeasurableSpace F
inst✝³ : BorelSpace F
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : SecondCountableTopologyEither E F
ν : Measure F
inst✝ : IsGaussian ν
L : StrongDual ℝ (E × F)
L₁ : E →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inl ℝ E F
hL₁ : L₁ = L ∘SL ContinuousLinearMap.inl ℝ E F
L₂ : F →L[ℝ] ℝ := L ∘SL ContinuousLinearMap.inr ℝ E F
hL₂ : L₂ = L ∘SL ContinuousLinearMap.inr ℝ E F
⊢ ↑(∫ (x : E), L₁ x ∂μ) + ↑(∫ (x : F), L₂ x ∂ν) = ↑(∫ (x : E × F), L x ∂μ.prod ν)
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
⊢ b < ‖p.1 + p.2‖ / √2 → (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖

Tactic:
hp2

Goal state after:
E : Type u_1
inst✝⁵ : SeminormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
μ : Measure E
inst✝ : SFinite μ
h : Measure.map (⇑(ContinuousLinearMap.rotation (-(π / 4)))) (μ.prod μ) = μ.prod μ
a b : ℝ
p : E × E
hp1 : ‖p.1 - p.2‖ / √2 ≤ a
hp2 : b < ‖p.1 + p.2‖ / √2
⊢ (b - a) / √2 < ‖p.1‖ ∧ (b - a) / √2 < ‖p.2‖
Module: Mathlib.Probability.Distributions.Fernique

Goal state before:
pp: c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 0 < logRatio c

Tactic:
refine div_pos (Real.log_pos ?_) (by positivity)

Goal state after:
c : ℝ≥0∞
hc_gt : 2⁻¹ < c
hc_lt : c < 1
⊢ 1 < c.toReal / (1 - c).toReal
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ cexp (-((∑ i, ↑⟪(stdOrthonormalBasis ℝ E) i, t⟫ ^ 2) / 2)) = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
← ofReal_pow,

Goal state after:
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ cexp (-((∑ x, ↑(⟪(stdOrthonormalBasis ℝ E) x, t⟫ ^ 2)) / 2)) = cexp (-↑(‖t‖ ^ 2) / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
t : E
⊢ charFun (stdGaussian E) t = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
rw [charFun_apply, stdGaussian, integral_map (Measurable.aemeasurable (by fun_prop))
    (Measurable.aestronglyMeasurable (by fun_prop))]
  simp_rw [sum_inner, ofReal_sum, Finset.sum_mul, exp_sum,
    integral_fintype_prod_eq_prod (f := fun i x ↦ exp (⟪x • stdOrthonormalBasis ℝ E i, t⟫ * I)),
    real_inner_smul_left, mul_comm _ (⟪_, _⟫), ofReal_mul, ← charFun_apply_real,
    charFun_gaussianReal]
  simp only [ofReal_zero, mul_zero, zero_mul, NNReal.coe_one, ofReal_one, one_mul,
    zero_sub]
  simp_rw [← exp_sum, Finset.sum_neg_distrib, ← Finset.sum_div, ← ofReal_pow,
    ← ofReal_sum, (stdOrthonormalBasis ℝ E).sum_sq_inner_right, neg_div]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.Multivariate

Goal state before:
pp: ι : Type u_1
inst✝ : Fintype ι
t : EuclideanSpace ℝ ι
⊢ cexp (∑ x, (↑(t.ofLp x) * ↑0 * I - ↑↑1 * ↑(t.ofLp x) ^ 2 / 2)) = cexp (-↑‖t‖ ^ 2 / 2)

Tactic:
← ofReal_pow,

Goal state after:
ι : Type u_1
inst✝ : Fintype ι
t : EuclideanSpace ℝ ι
⊢ cexp (∑ x, (↑(t.ofLp x) * ↑0 * I - ↑↑1 * ↑(t.ofLp x ^ 2) / 2)) = cexp (-↑(‖t‖ ^ 2) / 2)
Module: Mathlib.Probability.Distributions.Gaussian.Fernique

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hμ : ∫ (x : E), x ∂μ = 0
L✝ L : StrongDual ℝ E
⊢ ∫ (x : E), L x ∂μ = 0

Tactic:
simp [integral_dual, hμ]

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

Goal state before:
pp: E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : MeasurableSpace E
inst✝³ : BorelSpace E
μ : Measure E
inst✝² : IsGaussian μ
inst✝¹ : CompleteSpace E
inst✝ : SecondCountableTopology E
hμ : ∫ (x : E), x ∂μ = 0
θ : ℝ
L : StrongDual ℝ E
⊢ ∫ (x : E), L x ∂μ = 0

Tactic:
simp [integral_dual, hμ]

Goal state after:
Module: Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Basic

Goal state before:
pp: T : Type u_2
Ω : Type u_3
E : Type u_4
mΩ : MeasurableSpace Ω
P : Measure Ω
X : T → Ω → E
inst✝⁴ : NormedAddCommGroup E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : SecondCountableTopology E
hX : IsGaussianProcess X P
s t : T
⊢ HasGaussianLaw (fun ω ↦ (X s ω, X t ω)) P

Tactic:
exact (hX.hasGaussianLaw {s, t}).prodMk ⟨s, by simp⟩ ⟨t, by simp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → StieltjesFunction ℝ
inst✝ : IsFiniteKernel κ
hf : IsCondKernelCDF f κ ν
a : α
s : Set β
hs : MeasurableSet s
t✝ t : Set ℝ
ht : MeasurableSet t
iht : ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a = (κ a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) univ ∂ν a -
      ∫⁻ (b : β) in s, ((IsCondKernelCDF.toKernel f hf) (a, b)) t ∂ν a =
    (κ a) (s ×ˢ univ) - (κ a) (s ×ˢ t)

Tactic:
by
        rw [setLIntegral_toKernel_univ hf a hs, iht]

Goal state after:
Module: Mathlib.Probability.CondVar

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

Tactic:
obtain rfl | hc := eq_or_ne c 0

Goal state after:
case inl
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
⊢ Var[fun x ↦ 0; μ | m] = 0

case inr
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun x ↦ c; μ | m] = 0
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 : α
this :
  (((κ + η).withDensity fun a x ↦ ↑(1 - κ.rnDerivAux (κ + η) a x).toNNReal) a) {x | 1 ≤ κ.rnDerivAux (κ + η) a x} = 0
⊢ (η a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
rwa [withDensity_one_sub_rnDerivAux κ η] at this

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)
ν : Measure ((i : ι) → X i)
hν : ∀ (s : Finset ι) (t : (i : ι) → Set (X i)), (∀ (i : ι), MeasurableSet (t i)) → ν ((↑s).pi t) = ∏ i ∈ s, (μ i) (t i)
⊢ ν = infinitePi μ

Tactic:
refine (isProjectiveLimit_infinitePi μ).unique ?_ |>.symm
  refine fun s ↦ (pi_eq fun t ht ↦ ?_).symm
  classical
  rw [Measure.map_apply, restrict_preimage_univ, hν, ← prod_attach, univ_eq_attach]
  · congr with i
    rw [dif_pos i.2]
  any_goals fun_prop
  · rintro i
    split_ifs with hi
    · exact ht ⟨i, hi⟩
    · exact .univ
  · exact .univ_pi ht

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

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
κ : Kernel Ω 𝓧
μ : Measure Ω
inst✝⁶ : IsFiniteMeasure μ
inst✝⁵ : IsFiniteKernel κ
inst✝⁴ : StandardBorelSpace Ω
inst✝³ : Nonempty Ω
inst✝² : StandardBorelSpace 𝓧
inst✝¹ : Nonempty 𝓧
inst✝ : IsMarkovKernel κ
⊢ ⇑((κ†μ)†(⇑κ ∘ₘ μ)) =ᵐ[μ] ⇑κ

Tactic:
suffices κ =ᵐ[κ†μ ∘ₘ κ ∘ₘ μ] (κ†μ)†(κ ∘ₘ μ) by
    rw [posterior_comp_self] at this
    filter_upwards [this] with a h using h.symm
  refine ae_eq_posterior_of_compProd_eq_swap_comp κ ?_
  rw [posterior_comp_self, compProd_posterior_eq_swap_comp, Measure.comp_assoc,
    Kernel.swap_swap, Measure.id_comp]

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✝ : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ (infinitePi μ) (Set.univ.pi s) = ∏ i, (μ i) (s i)

Tactic:
rw [← coe_univ, infinitePi_pi]

Goal state after:
case mt
ι : Type u_1
X : ι → Type u_2
mX : (i : ι) → MeasurableSpace (X i)
μ : (i : ι) → Measure (X i)
hμ : ∀ (i : ι), IsProbabilityMeasure (μ i)
inst✝ : Fintype ι
s : (i : ι) → Set (X i)
hs : ∀ (i : ι), MeasurableSet (s i)
⊢ ∀ i ∈ univ, MeasurableSet (s i)
Module: Mathlib.Probability.Decision.Risk.Basic

Goal state before:
pp: case hf
Θ : 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 μ
⊢ AEMeasurable (uncurry fun x θ ↦ ℓ θ x * (P θ) Set.univ) (μ.prod π)

Tactic:
have := P.measurable_coe .univ
    fun_prop

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

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0

Tactic:
setLIntegral_congr_fun measurableSet_Iio
      (fun x (hx : x < 0) ↦ gammaPDF_of_neg hx),

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
⊢ ∫⁻ (x : ℝ) in Iio 0, 0 ∂volume = 0
Module: Mathlib.Probability.ProbabilityMassFunction.Basic

Goal state before:
pp: α : Type u_1
p : PMF α
⊢ p.toOuterMeasure.caratheodory = ⊤

Tactic:
refine eq_top_iff.2 <| le_trans (le_sInf fun x hx => ?_) (le_sum_caratheodory _)

Goal state after:
α : Type u_1
p : PMF α
x : MeasurableSpace α
hx : x ∈ Set.range fun i ↦ (p i • dirac i).caratheodory
⊢ ⊤ ≤ x
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r : ℝ
ht : 0 < t
hr : 0 < r
x : ℝ
⊢ ↑(cdf (paretoMeasure t r)) x = ∫ (x : ℝ) in Iic x, paretoPDFReal t r x

Tactic:
have : IsProbabilityMeasure (paretoMeasure t r) := isProbabilityMeasure_paretoMeasure ht hr
  rw [cdf_eq_real, paretoMeasure, measureReal_def, withDensity_apply _ measurableSet_Iic]
  refine (integral_eq_lintegral_of_nonneg_ae ?_ ?_).symm
  · exact ae_of_all _ fun _ ↦ by simp only [Pi.zero_apply, paretoPDFReal_nonneg ht.le hr.le]
  · fun_prop

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

Goal state before:
pp: r : ℝ≥0
n : ℕ
⊢ Po(r) {n} = ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)

Tactic:
poissonMeasure,

Goal state after:
r : ℝ≥0
n : ℕ
⊢ (Measure.sum fun n ↦ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) • Measure.dirac n) {n} =
    ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !)
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ Integrable f Po(r) ↔ Summable fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n ! * ‖f n‖

Tactic:
poissonMeasure,

Goal state after:
E : Type u_1
inst✝ : NormedAddCommGroup E
r : ℝ≥0
f : ℕ → E
⊢ Integrable f (Measure.sum fun n ↦ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) • Measure.dirac n) ↔
    Summable fun n ↦ rexp (-↑r) * ↑r ^ n / ↑n ! * ‖f n‖
Module: Mathlib.Probability.Distributions.Poisson.PoissonLimitThm

Goal state before:
pp: p : ℕ → ℝ
r : ℝ
k : ℕ
hr : Tendsto (fun n ↦ ↑n * p n) atTop (𝓝 r)
hp_lt_half : ∀ᶠ (n : ℕ) in atTop, p n < 1 / 2
n : ℕ
hn : k ≤ n
hne : p n < 1 / 2
⊢ (1 - p n) ^ (n - k) = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹

Tactic:
rw [pow_sub₀ _ (by grind) hn]

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ ∫ (n : ℕ), f n ∂Po(r) = ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n

Tactic:
poissonMeasure,

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : FiniteDimensional ℝ E
r : ℝ≥0
f : ℕ → E
⊢ (∫ (n : ℕ), f n ∂Measure.sum fun n ↦ ENNReal.ofReal (rexp (-↑r) * ↑r ^ n / ↑n !) • Measure.dirac n) =
    ∑' (n : ℕ), (rexp (-↑r) * ↑r ^ n / ↑n !) • f n
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
mX : AEMeasurable (fun ω i ↦ X i ω) P
h : ∀ (s : Finset ι), iIndepFun (s.restrict X) P
this✝ : IsProbabilityMeasure P
x✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun x ↦ X i x) P)
s : Finset ι
t : (i : ι) → Set (𝓧 i)
ht : ∀ (i : ι), MeasurableSet (t i)
this : (↑s).pi t = s.restrict ⁻¹' Set.univ.pi fun i ↦ t ↑i
⊢ (map (s.restrict ∘ fun ω i ↦ X i ω) P) (Set.univ.pi fun i ↦ t ↑i) = ∏ i ∈ s, (map (X i) P) (t i)

Tactic:
have : s.restrict ∘ (fun ω i ↦ X i ω) = fun ω i ↦ s.restrict X i ω := by ext; simp
    rw [this, (h s).map_fun_eq_pi_map, pi_pi]
    · simp only [Finset.restrict]
      rw [s.prod_coe_sort fun i ↦ P.map (X i) (t i)]
    exact fun i ↦ mX.eval i

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

Goal state before:
pp: α : Type u_1
s : Finset α
hs : s.Nonempty
⊢ ∀ (x : α), x ∈ (uniformOfFinset s hs).support ↔ x ∈ ↑s

Tactic:
let ⟨a, ha⟩ := hs

Goal state after:
α : Type u_1
s : Finset α
hs : s.Nonempty
a : α
ha : a ∈ s
⊢ ∀ (x : α), x ∈ (uniformOfFinset s ⋯).support ↔ x ∈ ↑s
Module: Mathlib.Probability.Independence.InfinitePi

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝¹ : IsProbabilityMeasure P
this✝ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
⊢ iIndepFun (fun p ω ↦ X p.fst p.snd ω) P

Tactic:
have : (MeasurableEquiv.piCurry 𝓧) ∘ (fun ω p ↦ X p.1 p.2 ω) = fun ω i j ↦ X i j ω := by
    ext; simp [Sigma.curry]

Goal state after:
ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
κ : ι → Type u_4
𝓧 : (i : ι) → κ i → Type u_5
m𝓧 : (i : ι) → (j : κ i) → MeasurableSpace (𝓧 i j)
X : (i : ι) → (j : κ i) → Ω → 𝓧 i j
mX : ∀ (i : ι) (j : κ i), Measurable (X i j)
h1 : iIndepFun (fun i ω x ↦ X i x ω) P
h2 : ∀ (i : ι), iIndepFun (X i) P
this✝² : IsProbabilityMeasure P
this✝¹ : ∀ (i : ι) (j : κ i), IsProbabilityMeasure (map (X i j) P)
this✝ : ∀ (i : ι), IsProbabilityMeasure (map (fun ω x ↦ X i x ω) P)
this : (⇑(MeasurableEquiv.piCurry 𝓧) ∘ fun ω p ↦ X p.fst p.snd ω) = fun ω i j ↦ X i j ω
⊢ iIndepFun (fun p ω ↦ X p.fst p.snd ω) P
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ eLpNorm (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω') < ∞

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top (mod_cast hp) (by simp),
      ENNReal.coe_toReal]

Goal state after:
case neg
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
p : ℝ≥0
ω' : Ω'
hi : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
t : ℝ
hp : ¬p = 0
⊢ ∫⁻ (a : Ω), ‖rexp (t * X a)‖ₑ ^ ↑p ∂κ ω' < ∞
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case refine_4
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ Tendsto (fun n ↦ truncation f n x) atTop (𝓝 (f x))

Tactic:
apply tendsto_const_nhds.congr' _

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
x : α
⊢ (fun x_1 ↦ f x) =ᶠ[atTop] fun n ↦ truncation f n x
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k✝ : Type u
G : Type v
V : Type u'
W : Type v'
inst✝⁸ : Monoid G
inst✝⁷ : Semiring k✝
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k✝ V
inst✝⁴ : AddCommGroup W
inst✝³ : Module k✝ W
σ✝ : Representation k✝ G V
ρ✝ : Representation k✝ G W
X Y Z : Action (Type w) G
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ ↑(MonoidAlgebra.tensorEquiv k).symm ∘ₗ (linearize k G (X ⊗ Y)) g =
    ((linearize k G X).tprod (linearize k G Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k).symm

Tactic:
by
    ext; simp [linearize_single _, MonoidAlgebra.tensorEquiv_symm_single_eq_single_one_tmul]; rfl

Goal state after: