mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Distributions.TwoValued

Goal state before:
pp: case inr
Ω : 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 Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [inst : IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1),
    Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]

Tactic:
obtain ⟨Y, hYmeas, hXY⟩ := ‹AEMeasurable[m₀] X μ›

Goal state after:
case inr
Ω : 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 Ω} (hm : m ≤ m₀) {μ : Measure Ω}
    [inst : IsFiniteMeasure μ] (hXmeas : AEMeasurable X μ) (hX : ∀ᵐ (ω : Ω) ∂μ, X ω = 0 ∨ X ω = 1),
    Measurable X → Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
hXmeas : ¬Measurable X
Y : Ω → ℝ
hYmeas : Measurable Y
hXY : X =ᵐ[μ] Y
⊢ Var[X; μ | m] =ᵐ[μ] μ[X | m] * μ[1 - X | m]
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
s : Set (𝓧 × 𝓨)
hs : MeasurableSet s
⊢ (Measure.map Z P ⊗ₘ κ.comap f hf) (Prod.map f id ⁻¹' s) = (Measure.map f (Measure.map Z P) ⊗ₘ κ) s

Tactic:
Measure.compProd_apply (by measurability),

Goal state after:
Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
s : Set (𝓧 × 𝓨)
hs : MeasurableSet s
⊢ ∫⁻ (a : 𝓩), ((κ.comap f hf) a) (Prod.mk a ⁻¹' Prod.map f id ⁻¹' s) ∂Measure.map Z P =
    (Measure.map f (Measure.map Z P) ⊗ₘ κ) s
Module: Mathlib.Probability.HasCondDistrib

Goal state before:
pp: Ω : Type u_1
𝓧 : Type u_2
𝓨 : Type u_3
𝓩 : Type u_4
mΩ : MeasurableSpace Ω
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
m𝓩 : MeasurableSpace 𝓩
P : Measure Ω
Y : Ω → 𝓨
κ : Kernel 𝓧 𝓨
inst✝¹ : SFinite P
inst✝ : IsSFiniteKernel κ
f : 𝓩 → 𝓧
hf : Measurable f
Z : Ω → 𝓩
h : HasCondDistrib Y Z (κ.comap f hf) P
⊢ Measure.map (Prod.map f id) (Measure.map Z P ⊗ₘ κ.comap f hf) = Measure.map f (Measure.map Z P) ⊗ₘ κ

Tactic:
by
        ext s hs
        rw [Measure.map_apply (by fun_prop) hs, Measure.compProd_apply (by measurability),
          Measure.compProd_apply hs, lintegral_map (Kernel.measurable_kernel_prodMk_left hs) hf]
        rfl

Goal state after:
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 μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω

Tactic:
← hst_eq,

Goal state after:
Ω : 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 μ
hs1_eq : ∀ s ∈ s1, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs2_eq : ∀ s ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) s).toReal) =ᵐ[μ] μ[s.indicator fun ω ↦ 1 | m']
hs12_eq :
  ∀ s ∈ s1, ∀ t ∈ s2, (fun ω ↦ (((condExpKernel μ m') ω) (s ∩ t)).toReal) =ᵐ[μ] μ[(s ∩ t).indicator fun ω ↦ 1 | m']
s t : Set Ω
h : ∀ᵐ (a : Ω) ∂μ.trim hm', ((condExpKernel μ m') a) (s ∩ t) = ((condExpKernel μ m') a) s * ((condExpKernel μ m') a) t
hs : s ∈ s1
ht : t ∈ s2
h'✝ : (fun x ↦ ((condExpKernel μ m') x) (s ∩ t)) =ᵐ[μ] fun x ↦ ((condExpKernel μ m') x) s * ((condExpKernel μ m') x) t
ω : Ω
hs_eq : (((condExpKernel μ m') ω) s).toReal = μ[s.indicator fun ω ↦ 1 | m'] ω
ht_eq : (((condExpKernel μ m') ω) t).toReal = μ[t.indicator fun ω ↦ 1 | m'] ω
hst_eq : (((condExpKernel μ m') ω) (s ∩ t)).toReal = μ[(s ∩ t).indicator fun ω ↦ 1 | m'] ω
h' : ((condExpKernel μ m') ω) (s ∩ t) = ((condExpKernel μ m') ω) s * ((condExpKernel μ m') ω) t
⊢ (((condExpKernel μ m') ω) (s ∩ t)).toReal = (μ[s.indicator fun ω ↦ 1 | m'] * μ[t.indicator fun ω ↦ 1 | m']) ω
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X₁✝ X₂✝ X₃✝ Y₁✝ Y₂✝ Y₃✝ : SFinKer
κ₁ : X₁✝ ⟶ Y₁✝
κ₂ : X₂✝ ⟶ Y₂✝
η : X₃✝ ⟶ Y₃✝
⊢ ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ })
          ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁ X₂✝ ≫
            (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝ X₂✝ Y₂✝ κ₂)
          X₃✝ ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ })
          { carrier := Y₁✝.carrier × Y₂✝.carrier, str := Prod.instMeasurableSpace } X₃✝ Y₃✝ η) ≫
      { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom =
    { hom := { hom := Kernel.deterministic ⇑prodAssoc ⋯, property := ⋯ },
          inv := { hom := Kernel.deterministic ⇑prodAssoc.symm ⋯, property := ⋯ }, hom_inv_id := ⋯,
          inv_hom_id := ⋯ }.hom ≫
      (fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₁
          { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace } ≫
        (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₁✝
          { carrier := X₂✝.carrier × X₃✝.carrier, str := Prod.instMeasurableSpace }
          { carrier := Y₂✝.carrier × Y₃✝.carrier, str := Prod.instMeasurableSpace }
          ((fun {X₁ X₂} κ Y ↦ { hom := κ.hom ∥ₖ Kernel.id, property := ⋯ }) κ₂ X₃✝ ≫
            (fun X Y₁ Y₂ κ ↦ { hom := Kernel.id ∥ₖ κ.hom, property := ⋯ }) Y₂✝ X₃✝ Y₃✝ η)

Tactic:
by
    ext : 1; dsimp
    simp only [Kernel.id_parallelComp_comp_parallelComp_id]
    rw [Kernel.deterministic_comp_eq_map, Kernel.comp_deterministic_eq_comap]
    ext _ _ hs
    rw [Kernel.map_apply' _ (by fun_prop) _ hs, Kernel.comap_apply' _ (by fun_prop)]
    repeat rw [Kernel.parallelComp_apply]
    rw [Measure.prod_apply hs, Measure.prod_apply (by measurability), lintegral_prod]
    · congr with a
      rw [Measure.prod_apply (by measurability)]
      rfl
    · refine Measurable.aemeasurable ?_
      exact measurable_measure_prodMk_left (by measurability)

Goal state after:
Module: Mathlib.Probability.Kernel.Category.SFinKer

Goal state before:
pp: X Y : SFinKer
a✝¹ : X.carrier × Y.carrier
s✝ : Set PUnit.{u + 1}
a✝ : MeasurableSet s✝
⊢ ((Kernel.discard (X.carrier × Y.carrier)) a✝¹) s✝ =
    (((Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier).map Prod.snd) a✝¹) s✝

Tactic:
Kernel.map_apply _ (by fun_prop),

Goal state after:
X Y : SFinKer
a✝¹ : X.carrier × Y.carrier
s✝ : Set PUnit.{u + 1}
a✝ : MeasurableSet s✝
⊢ ((Kernel.discard (X.carrier × Y.carrier)) a✝¹) s✝ =
    (Measure.map Prod.snd ((Kernel.discard X.carrier ∥ₖ Kernel.discard Y.carrier) a✝¹)) s✝
Module: Mathlib.Probability.Kernel.Representation

Goal state before:
pp: case e_6.mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
⊢ f a ξ ≤ x

Tactic:
simp only [sSup_le_iff, f]

Goal state after:
case e_6.mpr
X : Type u_1
mX : MeasurableSpace X
κ : Kernel X ↑I
inst✝ : IsMarkovKernel κ
f : X → ↑I → ↑I := fun s t ↦ sSup {x | (κ s).real (Icc 0 x) < ↑t}
measurable_f : Measurable (uncurry f)
a : X
x : ↑I
Iic_to_Icc : Iic x = Icc 0 x
κ_in_I : (κ a).real (Icc 0 x) ∈ I
ξ : ↑I
hξ : ↑ξ ≤ (κ a).real (Icc 0 x)
⊢ ∀ b ∈ {x | (κ a).real (Icc 0 x) < ↑ξ}, b ≤ x
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 κ ν
ε : ℝ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), 0 ≤ t → (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)

Tactic:
filter_upwards [h.mgf_le, h.ae_forall_integrable_exp_mul, h.isFiniteMeasure] with ω' h1 h2 _ t ht

Goal state after:
Ω : 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
⊢ (κ ω').real {ω | ε ≤ X ω} ≤ rexp (-t * ε + ↑c * t ^ 2 / 2)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : AEStronglyMeasurable f μ
A : ℝ
⊢ AEStronglyMeasurable ((Set.Ioc (-A) A).indicator id) (Measure.map f μ)

Tactic:
exact (stronglyMeasurable_id.indicator measurableSet_Ioc).aestronglyMeasurable

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

Goal state before:
pp: case pos.integrable_exp_mul
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * Y ω)) (⇑(prodMkLeft Ω' η) ∘ₘ ν ⊗ₘ κ)

pp: case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)

Tactic:
· simpa using h.integrable_exp_mul

Goal state after:
case pos.mgf_le
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
η : Kernel Ω Ω''
h : HasSubgaussianMGF Y cY η (⇑κ ∘ₘ ν)
hν : SFinite ν
hκ : IsSFiniteKernel κ
⊢ ∀ᵐ (ω' : Ω' × Ω) ∂ν ⊗ₘ κ, ∀ (t : ℝ), mgf Y ((prodMkLeft Ω' η) ω') t ≤ rexp (↑cY * t ^ 2 / 2)
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case h_meas
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
s : Finset ι
h_subG : ∀ i ∈ s, HasSubgaussianMGF (X i) (c i) μ
⊢ ∀ (i : ↥s), AEMeasurable (X ↑i) μ

Tactic:
exact fun i ↦ (h_subG i i.2).aemeasurable

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: 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) * ε

Tactic:
apply mul_pos (Nat.cast_pos.2 _) εpos
          refine zero_lt_one.trans_le ?_
          apply Nat.le_floor
          rw [Nat.cast_one]
          apply one_le_pow₀ c_one.le

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
⊢ ∀ᵐ (ω : Ω), (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n

Tactic:
have A : (∑' j : ℕ, ℙ {ω | X j ω ∈ Set.Ioi (j : ℝ)}) < ∞ := by
    convert! tsum_prob_mem_Ioi_lt_top hint (hnonneg 0) using 2
    ext1 j
    exact (hident j).measure_mem_eq measurableSet_Ioi
  have B : ∀ᵐ ω, Tendsto (fun n : ℕ => truncation (X n) n ω - X n ω) atTop (𝓝 0) := by
    filter_upwards [ae_eventually_notMem A.ne] with ω hω
    apply tendsto_const_nhds.congr' _
    filter_upwards [hω, Ioi_mem_atTop 0] with n hn npos
    simp only [truncation, indicator, Set.mem_Ioc, id, Function.comp_apply]
    split_ifs with h
    · exact (sub_self _).symm
    · have : -(n : ℝ) < X n ω := by
        apply lt_of_lt_of_le _ (hnonneg n ω)
        simpa only [Right.neg_neg_iff, Nat.cast_pos] using! npos
      simp only [this, true_and, not_le] at h
      exact (hn h).elim
  filter_upwards [B] with ω hω
  convert! isLittleO_sum_range_of_tendsto_zero hω using 1
  ext n
  rw [sum_sub_distrib]

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
H : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) =o[atTop] fun _x ↦ 1

Tactic:
convert! L.mul_isBigO (isBigO_refl (fun n : ℕ => (⌊c ^ n⌋₊ : ℝ)⁻¹) atTop) using 1

Goal state after:
case e'_7
Ω : 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 : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun x ↦ (∑ i ∈ range ⌊c ^ x⌋₊, X i ω) / ↑⌊c ^ x⌋₊ - ∫ (a : Ω), X 0 a) = fun x ↦
    (∑ i ∈ range ⌊c ^ x⌋₊, X i ω - ↑⌊c ^ x⌋₊ * ∫ (a : Ω), X 0 a) * (↑⌊c ^ x⌋₊)⁻¹

case e'_8
Ω : 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 : ∀ (n : ℕ), 0 < ↑⌊c ^ n⌋₊
ω : Ω
hω : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, truncation (X i) (↑i) ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
h'ω : (fun n ↦ ∑ i ∈ range n, truncation (X i) (↑i) ω - ∑ i ∈ range n, X i ω) =o[atTop] fun n ↦ ↑n
L : (fun n ↦ ∑ i ∈ range ⌊c ^ n⌋₊, X i ω - ↑⌊c ^ n⌋₊ * ∫ (a : Ω), X 0 a) =o[atTop] fun n ↦ ↑⌊c ^ n⌋₊
⊢ (fun _x ↦ 1) = fun x ↦ ↑⌊c ^ x⌋₊ * (↑⌊c ^ x⌋₊)⁻¹
Module: Mathlib.RepresentationTheory.Character

Goal state before:
pp: case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| V.character x✝⁻¹ * W.character x✝

Tactic:
← FDRep.char_linHom

Goal state after:
case a.f
k : Type u
inst✝³ : Field k
G : Type v
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Nat.card G)
V W : FDRep k G
x✝ : G
| (of (linHom V.ρ W.ρ)).character x✝
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁵ : IsProbabilityMeasure μ
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) μ
h' : StronglyMeasurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
s : Set E := Set.range (X 0) ∪ {0}
zero_s : 0 ∈ s
this✝ : SeparableSpace ↑s
this : Nonempty ↑s
φ : ℕ → SimpleFunc E E := SimpleFunc.nearestPt fun k ↦ Nat.casesOn k 0 (Subtype.val ∘ denseSeq ↑s)
Y : ℕ → ℕ → Ω → E := fun k i ↦ ⇑(φ k) ∘ X i
A : ∀ᵐ (ω : Ω) ∂μ, ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
B :
  ∀ᵐ (ω : Ω) ∂μ,
    ∀ (k : ℕ),
      Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop
        (𝓝 (∫ (x : Ω), (fun ω ↦ ‖(X 0 - Y k 0) ω‖) x ∂μ))
ω : Ω
hω : ∀ (k : ℕ), Tendsto (fun n ↦ (↑n)⁻¹ • ∑ i ∈ Finset.range n, Y k i ω) atTop (𝓝 (∫ (x : Ω), Y k 0 x ∂μ))
h'ω :
  ∀ (k : ℕ),
    Tendsto (fun n ↦ (∑ i ∈ Finset.range n, ‖(X i - Y k i) ω‖) / ↑n) atTop (𝓝 (∫ (x : Ω), ‖(X 0 - Y k 0) x‖ ∂μ))
ε : ℝ
εpos : 0 < ε
δ : ℝ
δpos : 0 < δ
hδ : δ + δ + δ < ε
⊢ ∃ k, ∫ (ω : Ω), ‖Y k 0 ω - X 0 ω‖ ∂μ < δ

Tactic:
exact ((tendsto_order.1 (tendsto_integral_norm_approxOn_sub h'.measurable hint)).2 δ
      δpos).exists

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic

Goal state before:
pp: case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.hom ≫ (freeLiftLEquiv k G (Fin (n + 1) → G) A).toModuleIso.inv

pp: case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)

pp: case a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

pp: case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv

pp: case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d n (n + 1)

Tactic:
Iso.hom_inv_id

Goal state after:
case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| 𝟙 (((barComplex k G).linearYonedaObj k A).X (n + 1))

case a.a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d (n + 1) (n + 1 + 1)

case a.a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin (n + 1 + 1) → G) A).toModuleIso.hom

case a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| (freeLiftLEquiv k G (Fin n → G) A).toModuleIso.inv

case a.a
k G : Type u
inst✝¹ : CommRing k
n✝ : ℕ
inst✝ : Group G
A : Rep k G
n : ℕ
| ((barComplex k G).linearYonedaObj k A).d n (n + 1)
Module: Mathlib.RepresentationTheory.Homological.GroupHomology.Basic

Goal state before:
pp: case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.hom ≫
    (A.coinvariantsTensorFreeLEquiv (Fin (n + 1) → G)).toModuleIso.inv

pp: case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n

pp: case a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

pp: case a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv

pp: case a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1)

Tactic:
Iso.hom_inv_id

Goal state after:
case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| 𝟙 ((HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).X (n + 1))

case a.a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1) n

case a.a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin n → G)).toModuleIso.hom

case a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (A.coinvariantsTensorFreeLEquiv (Fin (n + 1 + 1) → G)).toModuleIso.inv

case a.a
k✝ G✝ : Type u
inst✝³ : CommRing k✝
inst✝² : Group G✝
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
n✝ n : ℕ
| (HomologicalComplex.coinvariantsTensorObj A (barComplex k G)).d (n + 1 + 1) (n + 1)
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B C : Rep k G
φ : A ⟶ B
ψ : B ⟶ C
n : ℕ
⊢ map (MonoidHom.id G) (φ ≫ ψ) n = map (MonoidHom.id G) φ n ≫ map (MonoidHom.id G) ψ n

Tactic:
by
  rw [map, cochainsMap_id_comp, HomologicalComplex.homologyMap_comp]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
⊢ M.tateNorm ≫ (inhomogeneousCochains M).d 0 1 = 0

Tactic:
by
  simp [tateNorm, eq_d₀₁_comp_inv M]

Goal state after:
Module: Mathlib.RepresentationTheory.Homological.TateCohomology.Basic

Goal state before:
pp: R G : Type u
inst✝² : CommRing R
inst✝¹ : Group G
inst✝ : Fintype G
M : Rep R G
X Y : Rep R G
φ : X ⟶ Y
⊢ tateComplex X ⟶ tateComplex Y

Tactic:
by
  refine CochainComplex.ConnectData.map _ _ (chainsMap (.id G) φ) (cochainsMap (.id G) φ) ?_
  ext
  simp [Rep.tateNorm_eq, Representation.norm, Rep.hom_comm_apply]

Goal state after: