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)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x) =
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c] (updateFinset x (Iic c) y) ∂((traj κ b).map (frestrictLe c)) (frestrictLe b x)

Tactic:
Kernel.map_apply,

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 c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x) =
    ∫ (y : (i : ↥(Iic c)) → X ↑i),
      ((traj κ a) x₀)[f | ↑piLE c]
        (updateFinset x (Iic c) y) ∂Measure.map (frestrictLe c) ((traj κ b) (frestrictLe b x))

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)
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
a b c : ℕ
hab : a ≤ b
hbc : b ≤ c
x₀ : (i : ↥(Iic a)) → X ↑i
f : ((n : ℕ) → X n) → E
i_cf : Integrable ((traj κ a) x₀)[f | ↑piLE c] ((traj κ a) x₀)
mcf : StronglyMeasurable ((traj κ a) x₀)[f | ↑piLE c]
x : (n : ℕ) → X n
h1 : ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x = ((traj κ a) x₀)[f | ↑piLE b] x
h2 :
  ((traj κ a) x₀)[((traj κ a) x₀)[f | ↑piLE c] | ↑piLE b] x =
    ∫ (y : (n : ℕ) → X n), ((traj κ a) x₀)[f | ↑piLE c] y ∂(traj κ b) (frestrictLe b x)
⊢ Measurable (frestrictLe c)
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:
pow_sub₀ _ (by grind) hn

Goal state after:
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 * ((1 - p n) ^ k)⁻¹ = (1 - p n) ^ n * ((1 - p n) ^ k)⁻¹
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ Y =ᵐ[μ] X

Tactic:
filter_upwards [hXY] with ω hω; simp [hω]

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

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
m₀ : MeasurableSpace Ω
hm : m ≤ m₀
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hXmeas✝ : AEMeasurable X μ
hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1
this :
  ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {m₀ : MeasurableSpace Ω},
    m ≤ m₀ →
      ∀ {μ : Measure Ω} [IsFiniteMeasure μ],
        AEMeasurable X μ →
          (∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1) → Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ 1 - Y =ᵐ[μ] 1 - X

Tactic:
filter_upwards [hXY] with ω hω; simp [hω]

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

Goal state before:
pp: case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this : HasPDF X ℙ μ
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)

Tactic:
have : IsProbabilityMeasure ℙ := isProbabilityMeasure hns hnt hu

Goal state after:
case neg
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hms : MeasurableSet s
hu : IsUniform X s ℙ μ
hnt : ¬μ s = ∞
hns : ¬μ s = 0
this✝ : HasPDF X ℙ μ
this : IsProbabilityMeasure ℙ
⊢ pdf X ℙ μ =ᵐ[μ] s.indicator ((μ s)⁻¹ • 1)
Module: Mathlib.Probability.Distributions.Uniform

Goal state before:
pp: α : Type u_1
s : Multiset α
hs : s ≠ 0
⊢ (↑s.card)⁻¹ * ∑ b ∈ s.toFinset, ↑(Multiset.count b s) = 1

Tactic:
by
          rw [← Nat.cast_sum, Multiset.toFinset_sum_count_eq s,
            ENNReal.inv_mul_cancel (Nat.cast_ne_zero.2 (hs ∘ Multiset.card_eq_zero.1))
              (ENNReal.natCast_ne_top _)]

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

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

Tactic:
ae_ball_iff (Finset.countable_toSet s)

Goal state after:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
π : ι → Set (Set Ω)
hπ : ∀ (i : ι), ∀ s ∈ π i, MeasurableSet s
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
h_eq' :
  ∀ (s : Finset ι) (f : ι → Set Ω),
    (∀ i ∈ s, f i ∈ π i) →
      ∀ i ∈ s, (fun ω ↦ (((condExpKernel μ m') ω) (f i)).toReal) =ᵐ[μ] μ[(f i).indicator fun ω ↦ 1 | m']
s : Finset ι
f : ι → Set Ω
H : ∀ i ∈ s, f i ∈ π i
⊢ ∀ i ∈ ↑s, ∀ᵐ (x : Ω) ∂μ, (((condExpKernel μ m') x) (f i)).toReal = μ[(f i).indicator fun ω ↦ 1 | m'] x
Module: Mathlib.Probability.Independence.Conditional

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

Tactic:
simp only [CondIndepSets, Kernel.IndepSets]
  have hs1_eq : ∀ s ∈ s1, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs1 s hs)
  have hs2_eq : ∀ s ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω s)) =ᵐ[μ] μ⟦s | m'⟧ :=
    fun s hs ↦ condExpKernel_ae_eq_condExp hm' (hs2 s hs)
  have hs12_eq : ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ ENNReal.toReal (condExpKernel μ m' ω (s ∩ t)))
      =ᵐ[μ] μ⟦s ∩ t | m'⟧ :=
    fun s hs t ht ↦ condExpKernel_ae_eq_condExp hm' ((hs1 s hs).inter ((hs2 t ht)))
  refine ⟨fun h s t hs ht ↦ ?_, fun h s t hs ht ↦ ?_⟩ <;> specialize h s t hs ht
  · have h' := ae_eq_of_ae_eq_trim h
    filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h'] with ω hs_eq ht_eq hst_eq h'
    rw [← hst_eq, Pi.mul_apply, ← hs_eq, ← ht_eq, h', ENNReal.toReal_mul]
  · refine ((stronglyMeasurable_condExpKernel ((hs1 s hs).inter (hs2 t ht))).ae_eq_trim_iff hm'
      ((measurable_condExpKernel (hs1 s hs)).fun_mul
        (measurable_condExpKernel (hs2 t ht))).stronglyMeasurable).mpr ?_
    filter_upwards [hs1_eq s hs, hs2_eq t ht, hs12_eq s hs t ht, h] with ω hs_eq ht_eq hst_eq h
    have h_ne_top : condExpKernel μ m' ω (s ∩ t) ≠ ∞ := measure_ne_top (condExpKernel μ m' ω) _
    rw [← ENNReal.ofReal_toReal h_ne_top, hst_eq, h, Pi.mul_apply, ← hs_eq, ← ht_eq,
      ← ENNReal.toReal_mul, ENNReal.ofReal_toReal]
    exact ENNReal.mul_ne_top (measure_ne_top (condExpKernel μ m' ω) s)
      (measure_ne_top (condExpKernel μ m' ω) t)

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

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

Tactic:
simp only [iCondIndepFun_iff_iCondIndep]
  rw [iCondIndep_iff]
  exact fun i ↦ (hf i).comap_le

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - ∫ (x : Ω), X x ∂μ.tilted fun x ↦ t * X x) ^ 2 ∂μ.tilted fun x ↦ t * X x) =
    iteratedDeriv 2 (cgf X μ) t

Tactic:
integral_tilted_mul_self ht,

Goal state after:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ (∫ (ω : Ω), (X ω - deriv (cgf X μ) t) ^ 2 ∂μ.tilted fun x ↦ t * X x) = iteratedDeriv 2 (cgf X μ) t
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case mp
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
h : HasSubgaussianMGF X 0 κ ν
ω : Ω
⊢ 0 < X ω → ∃ a, 0 < a ∧ ↑a ≤ X ω

Tactic:
intro hp
      obtain ⟨q, h1, h2⟩ := exists_rat_btwn hp
      exact ⟨q, (q.cast_pos.1 h1), h2.le⟩

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: A : Type u_1
G : Type u_2
W : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
N : Submodule A[G] M
g : G
v : RestrictScalars A A[G] M
hv : v ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }
⊢ ((Representation.ofModule M) g) v ∈ { toAddSubmonoid := N.toAddSubmonoid, smul_mem' := ⋯ }

Tactic:
simpa [Representation.ofModule, RestrictScalars.lsmul] using!
      Submodule.smul_of_tower_mem N (MonoidAlgebra.single g 1) hv

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
α : Type u_1
f : α → ℝ
A : ℝ
h : ∀ (x : α), 0 ≤ f x
x : α
hx : 0 < f x
h'x : f x ≤ A
⊢ (if -A < f x ∧ f x ≤ A then f x else 0) = if True ∧ f x ≤ A then f x else 0

Tactic:
have : -A < f x := by linarith [h x]
      simp only [this, true_and]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ = ∫ (y : ℝ) in -A..A, y ^ n ∂Measure.map f μ

pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)

Tactic:
intervalIntegral.integral_of_le,

Goal state after:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ ∫ (y : ℝ), (Set.Ioc (-A) A).indicator id y ^ n ∂Measure.map f μ = ∫ (x : ℝ) in Set.Ioc (-A) A, x ^ n ∂Measure.map f μ

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ -A ≤ A

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
hA : 0 ≤ A
n : ℕ
hn : n ≠ 0
M : MeasurableSet (Set.Ioc (-A) A)
⊢ AEStronglyMeasurable (fun z ↦ (Set.Ioc (-A) A).indicator id z ^ n) (Measure.map f μ)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
n : ℕ
hn : n ≠ 0
h'f : 0 ≤ f
⊢ ∫ (x : α), truncation f A x ^ n ∂μ = ∫ (y : ℝ) in 0..A, y ^ n ∂Measure.map f μ

Tactic:
have M : MeasurableSet (Set.Ioc 0 A) := measurableSet_Ioc
  have M' : MeasurableSet (Set.Ioc A 0) := measurableSet_Ioc
  rw [truncation_eq_of_nonneg h'f]
  change ∫ x, (fun z => indicator (Set.Ioc 0 A) id z ^ n) (f x) ∂μ = _
  rcases le_or_gt 0 A with (hA | hA)
  · rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_le hA,
      ← integral_indicator M]
    · simp only [indicator, zero_pow hn, id, ite_pow]
    · exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable
  · rw [← integral_map (f := fun z => _ ^ n) hf.aemeasurable, intervalIntegral.integral_of_ge hA.le,
      ← integral_indicator M']
    · simp only [Set.Ioc_eq_empty_of_le hA.le, zero_pow hn, Set.indicator_empty, integral_zero,
        zero_eq_neg]
      apply integral_eq_zero_of_ae
      have : ∀ᵐ x ∂Measure.map f μ, (0 : ℝ) ≤ x :=
        (ae_map_iff hf.aemeasurable measurableSet_Ici).2 (Eventually.of_forall h'f)
      filter_upwards [this] with x hx
      simp only [indicator, Set.mem_Ioc, Pi.zero_apply, ite_eq_right_iff, and_imp]
      intro _ h''x
      have : x = 0 := by linarith
      simp [this, zero_pow hn]
    · exact ((measurable_id.indicator M).pow_const n).aestronglyMeasurable

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

Goal state before:
pp: case pos.inr.refine_1
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
t : ℝ
hκ : IsSFiniteKernel κ
hη : IsMarkovKernel η
⊢ MemLp (fun ω ↦ rexp (t * X ω.1)) 2 (⇑(κ ⊗ₖ η) ∘ₘ ν)

Tactic:
have h := hX.memLp_exp_mul t 2
    simp only [ENNReal.coe_ofNat] at h
    have : κ ∘ₘ ν = ((κ ⊗ₖ η) ∘ₘ ν).map Prod.fst := by
      rw [Measure.map_comp _ _ measurable_fst, ← fst_eq, fst_compProd]
    rwa [this, memLp_map_measure_iff h.1 measurable_fst.aemeasurable] at h

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
⊢ ∑' (j : ℕ), ℙ {ω | X ω ∈ Set.Ioi ↑j} < ∞

Tactic:
suffices ∀ K : ℕ, ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)} ≤ ENNReal.ofReal (𝔼[X] + 1) from
    (le_of_tendsto_of_tendsto (ENNReal.tendsto_nat_tsum _) tendsto_const_nhds
      (Eventually.of_forall this)).trans_lt ENNReal.ofReal_lt_top

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
⊢ ∀ (K : ℕ), ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi ↑j} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
inst✝ : IsProbabilityMeasure μ
a b : ℝ
hm : AEMeasurable X μ
hb : ∀ᵐ (ω : Ω) ∂μ, X ω ∈ Set.Icc a b
hc : ∫ (x : Ω), X x ∂μ = 0
t : ℝ
ht : t < 0
⊢ mgf (-X) μ (-t) ≤ rexp ((↑‖-a - -b‖₊ / 2) ^ 2 * (-t) ^ 2 / 2)

Tactic:
apply ProbabilityTheory.mgf_le_of_mem_Icc_of_integral_eq_zero (hm.neg)
      · filter_upwards [hb] with ω ⟨hl, hr⟩ using ⟨neg_le_neg_iff.2 hr, neg_le_neg_iff.2 hl⟩
      · simp only [Pi.neg_apply]; rw [integral_neg, hc, neg_zero]
      · rwa [Left.neg_pos_iff]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h
Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := fun n ↦ truncation (X n) ↑n
S : ℕ → Ω → ℝ := fun n ↦ ∑ i ∈ range n, Y i
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := fun n ↦ ⌊c ^ n⌋₊
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := c ^ 5 * (c - 1)⁻¹ ^ 3 * (2 * ∫ (a : Ω), X 0 a)
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ ℙ {ω | ↑(u i) * ε ≤ |S (u i) ω - ∫ (a : Ω), S (u i) a|} ≤ ENNReal.ofReal (Var[S (u i); ℙ] / (↑(u i) * ε) ^ 2)

Tactic:
apply meas_ge_le_variance_div_sq

Goal state after:
case h.hX
Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ MemLp (S (u i)) 2 ℙ

case h.hc
Ω : 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
ε : ℝ
εpos : 0 < ε
c_pos : 0 < c
hX : ∀ (i : ℕ), AEStronglyMeasurable (X i) ℙ
A : ∀ (i : ℝ), StronglyMeasurable ((Set.Ioc (-i) i).indicator id)
Y : ℕ → Ω → ℝ := ⋯
S : ℕ → Ω → ℝ := ⋯
hS : S = fun n ↦ ∑ i ∈ range n, Y i
u : ℕ → ℕ := ⋯
u_mono : Monotone u
I1 : ∀ (K : ℕ), ∑ j ∈ range K, (↑j ^ 2)⁻¹ * Var[Y j; ℙ] ≤ 2 * ∫ (a : Ω), X 0 a
C : ℝ := ⋯
I2 : ∀ (N : ℕ), ∑ i ∈ range N, (↑(u i) ^ 2)⁻¹ * Var[S (u i); ℙ] ≤ C
N i : ℕ
a✝ : i ∈ range N
⊢ 0 < ↑(u i) * ε
Module: Mathlib.RepresentationTheory.Rep.Basic

Goal state before:
pp: k : Type u
G : Type v
inst✝⁷ : Semiring k
inst✝⁶ : Monoid G
X✝ Y✝ : Type w
inst✝⁵ : AddCommGroup X✝
inst✝⁴ : AddCommGroup Y✝
inst✝³ : Module k X✝
inst✝² : Module k Y✝
ρ : Representation k G X✝
σ : Representation k G Y✝
A B C : Rep k G
Z : Type w
inst✝¹ : AddCommGroup Z
inst✝ : Module k Z
τ : Representation k G Z
X Y : Rep k G
f : X ⟶ Y
x✝ : IsIso ((forget (Rep k G)).map f)
⊢ IsIso f

Tactic:
by
    let i := asIso ((forget (Rep.{w} k G)).map f)
    let e : X.ρ.Equiv Y.ρ := { f.hom, i.toEquiv with }
    exact (mkIso e).isIso_hom

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ✝ φ ψ : ρ.Equiv σ
h1 : ⇑φ.toContinuousLinearEquiv = ⇑ψ.toContinuousLinearEquiv
h2 : (↑φ.toContinuousLinearEquiv).invFun = (↑ψ.toContinuousLinearEquiv).invFun
⊢ φ = ψ

Tactic:
by cases φ; cases ψ; simp_all

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

Goal state before:
pp: R : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
U : Type u_5
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
inst✝³ : AddCommGroup U
inst✝² : Module R U
inst✝¹ : TopologicalSpace U
inst✝ : IsTopologicalAddGroup U
ρ : ContRepresentation R G V
σ : ContRepresentation R G W
τ : ContRepresentation R G U
φ✝ φ : ρ.Equiv σ
ψ : σ.Equiv τ
g : G
⊢ ↑(φ.trans ψ.toContinuousLinearEquiv) ∘SL ρ g = τ g ∘SL ↑(φ.trans ψ.toContinuousLinearEquiv)

Tactic:
rw [← ContinuousLinearEquiv.comp_coe, comp_assoc,
    φ.isIntertwining, ← comp_assoc, ψ.isIntertwining, comp_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝ : CommRing k
n : ℕ
c : Fin (n + 1) → G
⊢ (d k G n) (MonoidAlgebra.single c 1) = ∑ p, MonoidAlgebra.single (c ∘ p.succAbove) ((-1) ^ ↑p)

Tactic:
by
  simp [d]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.Resolution

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
⊢ (Hom.hom (linearizationOfMulActionIso k G (Fin (m + 1) → G)).inv)
      ((Hom.hom ((linearization k G).mapIso (Action.diagonalSuccIsoTensorTrivial G m)).inv)
        ((Hom.hom
            (Functor.Monoidal.μIso (linearization k G) (Action.leftRegular G) (Action.trivial G (Fin m → G))).symm.inv)
          ((Hom.hom
              (MonoidalCategory.tensorIso (linearizationOfMulActionIso k G G)
                  (linearizationTrivialIso k G (Fin m → G))).inv)
            ((Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)))))) =
    MonoidAlgebra.single (g • Fin.partialProd f) r

Tactic:
step1

Goal state after:
k G : Type u
inst✝¹ : CommRing k
n : ℕ
inst✝ : Group G
i : Fin (n + 1) → G
eq3 :
  MonoidAlgebra.single (i 0 • Fin.partialProd fun i_1 ↦ i i_1.succ) 1 =
    MonoidAlgebra.single (Fin.partialProd i ∘ Fin.succ) 1
m : ℕ
f : Fin m → G
g : G
r : k
step1 :
  (Hom.hom (leftRegularTensorTrivialIsoFree k G (Fin m → G)).inv) (single f (MonoidAlgebra.single g r)) =
    MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r
⊢ (Hom.hom (linearizationOfMulActionIso k G (Fin (m + 1) → G)).inv)
      ((Hom.hom ((linearization k G).mapIso (Action.diagonalSuccIsoTensorTrivial G m)).inv)
        ((Hom.hom
            (Functor.Monoidal.μIso (linearization k G) (Action.leftRegular G) (Action.trivial G (Fin m → G))).symm.inv)
          ((Hom.hom
              (MonoidalCategory.tensorIso (linearizationOfMulActionIso k G G)
                  (linearizationTrivialIso k G (Fin m → G))).inv)
            (MonoidAlgebra.single g 1 ⊗ₜ[k] MonoidAlgebra.single f r)))) =
    MonoidAlgebra.single (g • Fin.partialProd f) r
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n : ℕ
g : Fin (n + 1) → G
a : ↑A
⊢ (ConcreteCategory.hom (d A n)) (single g a) =
    single (fun i ↦ g i.succ) ((A.ρ (g 0)⁻¹) a) +
      ∑ j, (-1) ^ (↑j + 1) • single (j.contractNth (fun x1 x2 ↦ x1 * x2) g) a

Tactic:
by
  simp [d]

Goal state after: