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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), ((traj κ b) a) (Prod.mk a ⁻¹' s) ∂(partialTraj κ a b) u =
    ((traj κ a) u) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

pp: case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, x)

pp: 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

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)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ ∫⁻ (a : (i : ↥(Iic b)) → X ↑i), ((traj κ b) a) (Prod.mk a ⁻¹' s) ∂(partialTraj κ a b) u =
    ((traj κ b ∘ₖ partialTraj κ a b) u) ((fun x ↦ (frestrictLe b x, x)) ⁻¹' s)

X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s

case hf
X : ℕ → Type u_1
inst✝¹ : (n : ℕ) → MeasurableSpace (X n)
κ : (n : ℕ) → Kernel ((i : ↥(Iic n)) → X ↑i) (X (n + 1))
inst✝ : ∀ (n : ℕ), IsMarkovKernel (κ n)
a b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ Measurable fun x ↦ (frestrictLe b x, 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 b : ℕ
hab : a ≤ b
u : (i : ↥(Iic a)) → X ↑i
s : Set (((i : ↥(Iic b)) → X ↑i) × ((n : ℕ) → X n))
ms : MeasurableSet s
⊢ MeasurableSet s
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
x : ℝ
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

Tactic:
by_cases h : γ = 0

Goal state after:
case pos
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : γ = 0
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹

case neg
x₀ : ℝ
γ : ℝ≥0
x : ℝ
h : ¬γ = 0
⊢ π⁻¹ * ↑γ * ((x - x₀) ^ 2 + ↑γ ^ 2)⁻¹ = π⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹
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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
⊢ Integrable (uncurry fun x ↦ f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)

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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
⊢ Integrable (uncurry fun x ↦ f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ ∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x) = 1

Tactic:
← ENNReal.toReal_eq_one_iff,

Goal state after:
x₀ : ℝ
γ : ℝ≥0
hγ : γ ≠ 0
⊢ (∫⁻ (x : ℝ), ENNReal.ofReal (cauchyPDFReal x₀ γ x)).toReal = 1
Module: Mathlib.Probability.Distributions.Cauchy

Goal state before:
pp: x₀ : ℝ
γ : ℝ≥0
⊢ (cauchyMeasure x₀ γ) Set.univ = 1

Tactic:
by_cases h : γ = 0

Goal state after:
case pos
x₀ : ℝ
γ : ℝ≥0
h : γ = 0
⊢ (cauchyMeasure x₀ γ) Set.univ = 1

case neg
x₀ : ℝ
γ : ℝ≥0
h : ¬γ = 0
⊢ (cauchyMeasure x₀ γ) Set.univ = 1
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ ∫⁻ (x : ℝ), gammaPDF a r x = 1

Tactic:
← ENNReal.toReal_eq_one_iff,

Goal state after:
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ (∫⁻ (x : ℝ), gammaPDF a r x).toReal = 1
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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ a) x₀)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x ↦ f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)

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
a b : ℕ
hab : a ≤ b
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
hf : Integrable f ((traj κ b ∘ₖ partialTraj κ a b) x₀)
A : Set ((i : ↥(Iic b)) → X ↑i)
hA : MeasurableSet A
⊢ Integrable (uncurry fun x ↦ f) ((partialTraj κ a b) x₀ ⊗ₘ traj κ b)
Module: Mathlib.Probability.Distributions.Gamma

Goal state before:
pp: case hf
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ 0 ≤ᵐ[volume.restrict (Ici 0)] fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))

pp: case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))

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

Goal state after:
case hfm
a r : ℝ
ha : 0 < a
hr : 0 < r
leftSide : ∫⁻ (x : ℝ) in Iio 0, gammaPDF a r x = 0
rightSide :
  ∫⁻ (x : ℝ) in Ici 0, gammaPDF a r x =
    ∫⁻ (x : ℝ) in Ici 0, ENNReal.ofReal (r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x)))
⊢ AEStronglyMeasurable (fun x ↦ r ^ a / Gamma a * x ^ (a - 1) * rexp (-(r * x))) (volume.restrict (Ici 0))
Module: Mathlib.Probability.Distributions.Pareto

Goal state before:
pp: t r x : ℝ
hx : x ≤ t
a : ℝ
a✝ : a < x
⊢ paretoPDF t r a = (fun x ↦ 0) a

Tactic:
simp only [paretoPDF_eq, ENNReal.ofReal_eq_zero]

Goal state after:
t r x : ℝ
hx : x ≤ t
a : ℝ
a✝ : a < x
⊢ (if t ≤ a then r * t ^ r * a ^ (-(r + 1)) else 0) ≤ 0
Module: Mathlib.Probability.Distributions.Pareto

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

Tactic:
← ENNReal.toReal_eq_one_iff,

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

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ ((pure a).bindOnSupport f) b = (f a ⋯) b

Tactic:
simp only [bindOnSupport_apply, pure_apply]

Goal state after:
α : Type u_1
β : Type u_2
a : α
f : (a' : α) → a' ∈ (pure a).support → PMF β
b : β
⊢ (∑' (a_1 : α), (if a_1 = a then 1 else 0) * if h : (if a_1 = a then 1 else 0) = 0 then 0 else (f a_1 h) b) = (f a ⋯) b
Module: Mathlib.Probability.Distributions.Poisson.Basic

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ ∑' (a : ℕ), ↑(rexp (-↑r) * ↑r ^ a / ↑a !) * cexp (↑(↑a * t) * I) =
    ∑' (a : ℕ), ↑(rexp (-↑r)) * ((↑↑r * cexp (↑t * I)) ^ a / ↑a !)

Tactic:
congr with a

Goal state after:
case e_f
r : ℝ≥0
t : ℝ
a : ℕ
⊢ ↑(rexp (-↑r) * ↑r ^ a / ↑a !) * cexp (↑(↑a * t) * I) = ↑(rexp (-↑r)) * ((↑↑r * cexp (↑t * I)) ^ a / ↑a !)
Module: Mathlib.Probability.ProbabilityMassFunction.Constructions

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
p : PMF α
s : Set α
h : ∃ a ∈ s, a ∈ p.support
⊢ tsum (s.indicator ⇑p) ≠ 0

Tactic:
simpa using h

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

Goal state before:
pp: r : ℝ≥0
t : ℝ
⊢ ↑(rexp (-↑r)) * cexp (↑↑r * cexp (↑t * I)) = cexp (↑↑r * (cexp (↑t * I) - 1))

Tactic:
rw [ofReal_exp, ← Complex.exp_add]
      push_cast
      ring_nf

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

Goal state before:
pp: case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᵐ[μ] 0

Tactic:
simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H,
    smul_zero] at hu

Goal state after:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : μ s = 0
hu : Measure.map X ℙ = 0
⊢ pdf X ℙ μ =ᵐ[μ] 0
Module: Mathlib.Probability.Kernel.Condexp

Goal state before:
pp: case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
⊢ Measure.map id μ ⊗ₘ (condDistrib id id μ).comap id ⋯ = Measure.map Function.diag μ

Tactic:
refine (congrArg _ (Kernel.ext fun a => Measure.ext fun s hs => ?_)).trans
    (compProd_map_condDistrib measurable_id.aemeasurable)

Goal state after:
case inr
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
h : Nonempty Ω
this : m ⊓ mΩ = m
a : Ω
s : Set Ω
hs : MeasurableSet s
⊢ (((condDistrib id id μ).comap id ⋯) a) s = ((condDistrib (fun a ↦ a) id μ) 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✝
⊢ ∫⁻ (x : Y₁✝.carrier),
      ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (x, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 ∂κ₁.hom a✝.1.1 =
    ∫⁻ (x : Y₁✝.carrier),
      ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2)) (Prod.mk x ⁻¹' s✝) ∂κ₁.hom (prodAssoc a✝).1

Tactic:
congr with a

Goal state after:
case e_f
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✝
a : Y₁✝.carrier
⊢ ∫⁻ (y : Y₂✝.carrier), (η.hom a✝.2) (Prod.mk (a, y) ⁻¹' ⇑prodAssoc ⁻¹' s✝) ∂κ₂.hom a✝.1.2 =
    ((κ₂.hom (prodAssoc a✝).2.1).prod (η.hom (prodAssoc a✝).2.2)) (Prod.mk a ⁻¹' s✝)
Module: Mathlib.Probability.Process.Kolmogorov

Goal state before:
pp: T : Type u_1
Ω : Type u_2
E : Type u_3
inst✝⁴ : PseudoEMetricSpace T
mΩ : MeasurableSpace Ω
inst✝³ : PseudoEMetricSpace E
p q : ℝ
M : ℝ≥0
P : Measure Ω
X : T → Ω → E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : SecondCountableTopology E
h_meas : ∀ (s : T), Measurable (X s)
h_kol : ∀ (s t : T), ∫⁻ (ω : Ω), edist (X s ω) (X t ω) ^ p ∂P ≤ ↑M * edist s t ^ q
hp : 0 < p
hq : 0 < q
s t : T
this : Measurable fun ω ↦ (X s ω, X t ω)
⊢ Measurable fun ω ↦ (X s ω, X t ω)

Tactic:
rwa [Prod.borelSpace.measurable_eq] at this

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c κ ν
ε : ℝ
ω' : Ω'
h1 : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
h2 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (κ ω')
a✝ : IsFiniteMeasure (κ ω')
t : ℝ
ht : 0 ≤ t
⊢ rexp (-t * ε) * mgf X (κ ω') t ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)

Tactic:
by
    rw [exp_add]
    gcongr
    exact h1 t

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

Goal state before:
pp: case h₁
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := ⋯
q : ℝ≥0 := ⋯
ω' : Ω'
hmX : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑cX * t ^ 2 / 2)
hmY : ∀ (t : ℝ), mgf Y (κ ω') t ≤ rexp (↑cY * t ^ 2 / 2)
hlX : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * X ω)) (↑p) (κ ω')
hlY : ∀ (t : ℝ), MemLp (fun ω ↦ rexp (t * Y ω)) (↑q) (κ ω')
t : ℝ
⊢ ∫ (x : Ω), rexp (t * ↑q * Y x) ∂κ ω' ≤ rexp (↑cY * (t * ↑q) ^ 2 / 2)

Tactic:
· exact hmY (t * q)

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
c : ℝ≥0
Ω' : Type u_2
mΩ' : MeasurableSpace Ω'
μ : Measure Ω'
Y : Ω' → Ω
X : Ω → ℝ
hY : AEMeasurable Y μ
h : HasSubgaussianMGF X c (Measure.map Y μ)
t : ℝ
⊢ mgf (X ∘ Y) μ t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
by
    convert! h.mgf_le t using 1
    rw [mgf_map hY (h.integrable_exp_mul t).1]

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
inst✝⁷ : Semiring A
inst✝⁶ : Monoid G
inst✝⁵ : AddCommMonoid V
inst✝⁴ : AddCommMonoid W
inst✝³ : AddCommMonoid U
inst✝² : Module A V
inst✝¹ : Module A W
inst✝ : Module A U
ρ : Representation A G V
σ : Representation A G W
τ : Representation A G U
f : V →ₗ[A] W
hf : ∀ (g : G) (v : V), f ((ρ g) v) = (σ g) (f v)
g : G
⊢ f ∘ₗ ρ g = σ g ∘ₗ f

Tactic:
by ext v; exact hf g v

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk.mk
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
toLinearMap✝¹ : V →ₗ[A] W
isIntertwining'✝¹ : ∀ (g : G), toLinearMap✝¹ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝¹
toLinearMap✝ : V →ₗ[A] W
isIntertwining'✝ : ∀ (g : G), toLinearMap✝ ∘ₗ ρ g = σ g ∘ₗ toLinearMap✝
h :
  { toLinearMap := toLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ }.toLinearMap =
    { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }.toLinearMap
⊢ { toLinearMap := toLinearMap✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toLinearMap := toLinearMap✝, isIntertwining' := isIntertwining'✝ }

Tactic:
simpa using h

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case mk'.mk'
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
toIntertwiningMap✝¹ : ρ.IntertwiningMap σ
invFun✝¹ : W → V
left_inv✝¹ : Function.LeftInverse invFun✝¹ toIntertwiningMap✝¹.toFun
right_inv✝¹ : Function.RightInverse invFun✝¹ toIntertwiningMap✝¹.toFun
toIntertwiningMap✝ : ρ.IntertwiningMap σ
invFun✝ : W → V
left_inv✝ : Function.LeftInverse invFun✝ toIntertwiningMap✝.toFun
right_inv✝ : Function.RightInverse invFun✝ toIntertwiningMap✝.toFun
h :
  ⇑{ toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    ⇑{ toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }
⊢ { toIntertwiningMap := toIntertwiningMap✝¹, invFun := invFun✝¹, left_inv := left_inv✝¹, right_inv := right_inv✝¹ } =
    { toIntertwiningMap := toIntertwiningMap✝, invFun := invFun✝, left_inv := left_inv✝, right_inv := right_inv✝ }

Tactic:
simpa using h

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

Goal state before:
pp: case mp
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
k : Type u
inst✝ : CommRing k
φ : H →* G
S : ShortComplex (Rep k G)
h : (S.map (resFunctor φ)).ShortExact
h₁ : S.Exact
h₂ : Function.Injective ⇑(Hom.hom (resMap φ S.f))
h₃ : Function.Surjective ⇑(Hom.hom (resMap φ S.g))
⊢ S.ShortExact

Tactic:
exact {exact := h₁, mono_f := mono_iff_injective _|>.2 h₂, epi_g := epi_iff_surjective _|>.2 h₃}

Goal state after:
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
f : G → k[G] := fun x ↦ single x 1
⊢ ⅟↑(Fintype.card G) • ∑ x, f (g * x) = ⅟↑(Fintype.card G) • ∑ x, f x

Tactic:
rw [Function.Bijective.sum_comp (Group.mulLeft_bijective g) _]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [I] with ω hω

Goal state after:
Ω : Type u_2
m : MeasurableSpace Ω
μ : Measure Ω
X : ℕ → Ω → ℝ
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
mΩ : MeasureSpace Ω := { toMeasurableSpace := m, volume := μ }
h : ∀ᵐ (ω : Ω), X 0 ω = 0
I : ∀ᵐ (ω : Ω), ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ (∑ i ∈ range n, X i ω) / ↑n) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
⊢ ∀ᵐ (ω : Ω) ∂μ, Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))

Tactic:
filter_upwards [I] with ω hω

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
X : ℕ → Ω → E
hint : Integrable (X 0) μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, X i ω) atTop (𝓝 (∫ (x : Ω), X 0 x ∂μ))
Module: Mathlib.RepresentationTheory.Coinvariants

Goal state before:
pp: k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
α : Type u
inst✝ : DecidableEq α
x : ↑A
i : α
g : G
r : k
⊢ (A.coinvariantsTensorFreeToFinsupp α)
      ((Coinvariants.mk (A.ρ.tprod (Representation.free k G α))) (x ⊗ₜ[k] single i (MonoidAlgebra.single g r))) =
    single i (r • (A.ρ g⁻¹) x)

Tactic:
by
  simp [coinvariantsTensorFreeToFinsupp, Representation.finsuppTensorRight]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
⊢ (fun ω ↦ (↑n)⁻¹ • ∑ i ∈ range n, X i ω) =ᵐ[μ] 0

Tactic:
filter_upwards [I] with ω hω

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
inst✝¹ : MeasurableSpace E
inst✝ : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
I : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), X i ω = 0
n : ℕ
ω : Ω
hω : ∀ (i : ℕ), X i ω = 0
⊢ (↑n)⁻¹ • ∑ i ∈ range n, X i ω = 0 ω
Module: Mathlib.RingTheory.SimpleModule.InjectiveProjective

Goal state before:
pp: R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = (h ∘ₗ f) x✝

Tactic:
LinearMap.comp_apply

Goal state after:
R : Type u_1
inst✝³ : Ring R
inst✝² : IsSemisimpleRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
X Y : Type u_2
x✝⁴ : AddCommGroup X
x✝³ : AddCommGroup Y
x✝² : Module R X
x✝¹ : Module R Y
f : X →ₗ[R] Y
hf : Function.Injective ⇑f
g : X →ₗ[R] M
h : Y →ₗ[R] M
comp : h ∘ₗ f = g
x✝ : X
⊢ h (f x✝) = h (f x✝)
Module: Mathlib.RepresentationTheory.Continuous.Basic

Goal state before:
pp: case mk''.mk''
R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁹ : Monoid G
inst✝⁸ : Ring R
inst✝⁷ : AddCommGroup V
inst✝⁶ : TopologicalSpace V
inst✝⁵ : IsTopologicalAddGroup V
inst✝⁴ : Module R V
inst✝³ : AddCommGroup W
inst✝² : TopologicalSpace W
inst✝¹ : IsTopologicalAddGroup W
inst✝ : Module R W
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
toContinuousLinearEquiv✝¹ : V ≃L[R] W
cont✝¹ : Continuous (↑↑toContinuousLinearEquiv✝¹).toFun
isIntertwining'✝¹ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝¹, cont := cont✝¹ }
toContinuousLinearEquiv✝ : V ≃L[R] W
cont✝ : Continuous (↑↑toContinuousLinearEquiv✝).toFun
isIntertwining'✝ :
  ∀ (g : G),
    { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ } ∘SL ρ g =
      σ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv✝, cont := cont✝ }
h :
  ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    ⇑{ toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }
⊢ { toContinuousLinearEquiv := toContinuousLinearEquiv✝¹, cont := cont✝¹, isIntertwining' := isIntertwining'✝¹ } =
    { toContinuousLinearEquiv := toContinuousLinearEquiv✝, cont := cont✝, isIntertwining' := isIntertwining'✝ }

Tactic:
simpa using h

Goal state after: