mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Probability.Independence.ZeroOne

Goal state before:
pp: case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : 1 * (κ a) (t ∩ t) = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ∞
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞

Tactic:
Set.inter_self,

Goal state after:
case neg
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
m0 : MeasurableSpace Ω
κ : Kernel α Ω
μα : Measure α
t : Set Ω
h_indep : ∀ᵐ (a : α) ∂μα, (κ a) (t ∩ t) = (κ a) t * (κ a) t
a : α
ha : 1 * (κ a) t = (κ a) t * (κ a) t
h0 : ¬(κ a) t = 0
h_top : ¬(κ a) t = ∞
⊢ (κ a) t = 0 ∨ (κ a) t = 1 ∨ (κ a) t = ∞
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' ∈ {s}
⊢ MeasurableSet s'

Tactic:
Set.mem_singleton_iff

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = s
⊢ MeasurableSet s'
Module: Mathlib.Probability.Independence.Conditional

Goal state before:
pp: Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' ∈ {t}
⊢ MeasurableSet s'

Tactic:
Set.mem_singleton_iff

Goal state after:
Ω : Type u_1
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
s t : Set Ω
hs : MeasurableSet s
ht : MeasurableSet t
s' : Set Ω
hs' : s' = t
⊢ MeasurableSet s'
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ

Tactic:
exp_sub,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / rexp (cgf X μ t)) ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a - cgf X μ t)) ∂μ

Tactic:
exp_sub,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
inst✝ : SFinite μ
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / mgf X μ t) ∂μ =
    ∫⁻ (a : Ω) in s, ENNReal.ofReal (rexp (t * X a) / rexp (cgf X μ t)) ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ

Tactic:
exp_sub,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
g : Ω → E
s : Set Ω
hs : MeasurableSet s
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ = ∫ (x : Ω) in s, (rexp (t * X x) / rexp (cgf X μ t)) • g x ∂μ
Module: Mathlib.Probability.Moments.Tilted

Goal state before:
pp: case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ = ∫ (x : Ω) in s, rexp (t * X x - cgf X μ t) • g x ∂μ

Tactic:
exp_sub,

Goal state after:
case inr
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
t : ℝ
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : SFinite μ
g : Ω → E
s : Set Ω
ht : Integrable (fun ω ↦ rexp (t * X ω)) μ
hμ : NeZero μ
⊢ ∫ (x : Ω) in s, (rexp (t * X x) / mgf X μ t) • g x ∂μ = ∫ (x : Ω) in s, (rexp (t * X x) / rexp (cgf X μ t)) • g x ∂μ
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
hX : IsKolmogorovProcess X P p q M
s t : T
⊢ StronglyMeasurable fun ω ↦ edist (X s ω) (X t ω)

Tactic:
borelize (E × E)
  exact continuous_edist.stronglyMeasurable.comp_measurable (hX.measurablePair s t)

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

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

Tactic:
exact h.integrable_exp_mul t

Goal state after:
Module: Mathlib.RepresentationTheory.Subrepresentation

Goal state before:
pp: case single
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
σ : Subrepresentation ρ
v : ρ.asModule
hv : v ∈ σ.toSubmodule.carrier
g : G
a : A
⊢ a • (ρ g) (ρ.asModuleEquiv v) ∈ σ.toSubmodule.carrier

Tactic:
exact σ.toSubmodule.smul_mem' a (σ.apply_mem_toSubmodule g hv)

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 Y : Ω → ℝ
cX cY : ℝ≥0
hX : HasSubgaussianMGF X cX κ ν
hY : HasSubgaussianMGF Y cY κ ν
hX0 : ¬cX = 0
hY0 : ¬cY = 0
p : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
⊢ ∀ᵐ (ω' : Ω') ∂ν,
    ∀ (t : ℝ), mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)

Tactic:
filter_upwards [hX.mgf_le, hY.mgf_le, hX.ae_forall_memLp_exp_mul p,
        hY.ae_forall_memLp_exp_mul q] with ω' hmX hmY hlX hlY t

Goal state after:
Ω : 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 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cX
q : ℝ≥0 := (NNReal.sqrt cX + NNReal.sqrt cY) / NNReal.sqrt cY
ω' : Ω'
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 : ℝ
⊢ mgf (fun ω ↦ X ω + Y ω) (κ ω') t ≤ rexp (↑((NNReal.sqrt cX + NNReal.sqrt cY) ^ 2) * t ^ 2 / 2)
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case pos
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∈ Set.Ioc (-A) A
⊢ |f x| ≤ |f x|

pp: case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|

Tactic:
· exact le_rfl

Goal state after:
case neg
α : Type u_1
f : α → ℝ
A : ℝ
x : α
h✝ : f x ∉ Set.Ioc (-A) A
⊢ |0| ≤ |f x|
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
⊢ Tendsto (fun A ↦ ∫ (x : α), truncation f A x ∂μ) atTop (𝓝 (∫ (x : α), f x ∂μ))

Tactic:
refine tendsto_integral_filter_of_dominated_convergence (fun x => abs (f x)) ?_ ?_ ?_ ?_
  · exact Eventually.of_forall fun A ↦ hf.aestronglyMeasurable.truncation
  · filter_upwards with A
    filter_upwards with x
    rw [Real.norm_eq_abs]
    exact abs_truncation_le_abs_self _ _ _
  · exact hf.abs
  · filter_upwards with x
    apply tendsto_const_nhds.congr' _
    filter_upwards [Ioi_mem_atTop (abs (f x))] with A hA
    exact (truncation_eq_self hA).symm

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)

Tactic:
have : IsProbabilityMeasure ρ := Measure.isProbabilityMeasure_map hint.aemeasurable

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := Measure.map X ℙ
this : IsProbabilityMeasure ρ
⊢ ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc ↑j ↑N} ≤ ENNReal.ofReal ((∫ (a : Ω), X a) + 1)
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:
by
  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
  intro K
  have A : Tendsto (fun N : ℕ => ∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioc (j : ℝ) N}) atTop
      (𝓝 (∑ j ∈ range K, ℙ {ω | X ω ∈ Set.Ioi (j : ℝ)})) := by
    refine tendsto_finsetSum _ fun i _ => ?_
    have : {ω | X ω ∈ Set.Ioi (i : ℝ)} = ⋃ N : ℕ, {ω | X ω ∈ Set.Ioc (i : ℝ) N} := by
      apply Set.Subset.antisymm _ _
      · intro ω hω
        obtain ⟨N, hN⟩ : ∃ N : ℕ, X ω ≤ N := exists_nat_ge (X ω)
        exact Set.mem_iUnion.2 ⟨N, hω, hN⟩
      · simp +contextual only [Set.mem_Ioc, Set.mem_Ioi,
          Set.iUnion_subset_iff, Set.ofPred_subset_ofPred, imp_true_iff]
    rw [this]
    apply tendsto_measure_iUnion_atTop
    intro m n hmn x hx
    exact ⟨hx.1, hx.2.trans (Nat.cast_le.2 hmn)⟩
  apply le_of_tendsto_of_tendsto A tendsto_const_nhds
  filter_upwards [Ici_mem_atTop K] with N hN
  exact sum_prob_mem_Ioc_le hint hnonneg hN

Goal state after:
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
g : G
⊢ ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1}) ∘ₗ (linearize k G (𝟙_ (Action (Type u) G))) g =
    (trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{u + 1})

Tactic:
ext; simp [linearize_single _]

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 / (↑k + 1) * x ^ 2 ∂ρ ≤ ∫ (x : ℝ) in Set.Ioc ↑k ↑(k + 1), 2 * x ∂ρ

Tactic:
refine setIntegral_mono_on ?_ ?_ measurableSet_Ioc fun x hx => ?_

Goal state after:
case h.refine_1
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ IntegrableOn (fun x ↦ 2 / (↑k + 1) * x ^ 2) (Set.Ioc ↑k ↑(k + 1)) ρ

case h.refine_2
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
⊢ IntegrableOn (HMul.hMul 2) (Set.Ioc ↑k ↑(k + 1)) ρ

case h.refine_3
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
k : ℕ
a✝ : k ∈ range K
Ik : ↑k ≤ ↑(k + 1)
x : ℝ
hx : x ∈ Set.Ioc ↑k ↑(k + 1)
⊢ 2 / (↑k + 1) * x ^ 2 ≤ 2 * x
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: case refine_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
hX : AEMeasurable X μ
h : HasSubgaussianMGF X c μ
t : ℝ
⊢ Integrable ((fun ω ↦ rexp (t * id ω)) ∘ X) μ

Tactic:
exact h.integrable_exp_mul t

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.inr
Ω : 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)
N j : ℕ
a✝ : j ∈ range (u (N - 1))
hj : 0 < j
⊢ (∑ i ∈ range N with j < u i, (↑(u i) ^ 2)⁻¹) * Var[Y j; ℙ] ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2 * Var[Y j; ℙ]

Tactic:
apply mul_le_mul_of_nonneg_right _ (variance_nonneg _ _)

Goal state after:
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : ℕ → Ω → ℝ
hint : Integrable (X 0) ℙ
hindep : Pairwise ((fun f g ↦ f ⟂ᵢ g) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) ℙ ℙ
hnonneg : ∀ (i : ℕ) (ω : Ω), 0 ≤ X i ω
c : ℝ
c_one : 1 < c
ε : ℝ
ε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 : ℝ := ⋯
N j : ℕ
a✝ : j ∈ range (u (N - 1))
hj : 0 < j
⊢ ∑ i ∈ range N with j < u i, (↑(u i) ^ 2)⁻¹ ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / ↑j ^ 2
Module: Mathlib.RepresentationTheory.Rep.Res

Goal state before:
pp: k✝ : Type u
inst✝³ : Semiring k✝
G : Type v1
H : Type v2
inst✝² : Monoid G
inst✝¹ : Monoid H
f : H →* G
M : Rep k✝ G
k : Type u
inst✝ : CommSemiring k
x✝³ x✝² : Rep k G
x✝¹ : x✝³ ⟶ x✝²
x✝ : k
⊢ (resFunctor f).map (x✝ • x✝¹) = x✝ • (resFunctor f).map x✝¹

Tactic:
by ext : 2; simp [smul_hom]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u_1
G : Type u_2
V : Type u_3
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup V
inst✝² : Module k V
ρ : Representation k G V
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
v : V
hv : ∀ (g : G), (ρ g) v = v
⊢ ρ.averageMap v = v

Tactic:
simp [average, map_sum, hv, Finset.card_univ, ← Nat.cast_smul_eq_nsmul k _ v, smul_smul]

Goal state after:
Module: Mathlib.RepresentationTheory.Invariants

Goal state before:
pp: k : Type u
G : Type v
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
S : Subgroup G
inst✝ : S.Normal
X : ModuleCat k
Y : Rep k G
f : (trivialFunctor k G).obj X ⟶ Y
c✝ : ↑((trivialFunctor k G).obj X)
g✝ : G
⊢ (Y.ρ g✝) ((Hom.hom f).toLinearMap c✝) = (Hom.hom f).toLinearMap c✝

Tactic:
exact (hom_comm_apply f _ _).symm

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case hint
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : IsProbabilityMeasure μ
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
inst✝ : MeasurableSpace E
X : ℕ → Ω → E
h' : Measurable (X 0)
hindep : Pairwise ((fun x1 x2 ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
φ : SimpleFunc E E
c : E
s : Set E
hs : MeasurableSet s
F : E → ℝ := ⋯
F_meas : Measurable F
Y : ℕ → Ω → ℝ := ⋯
⊢ Integrable (Y 0) μ

Tactic:
exact SimpleFunc.integrable_of_isFiniteMeasure
          ((SimpleFunc.piecewise s hs (SimpleFunc.const _ (1 : ℝ))
            (SimpleFunc.const _ (0 : ℝ))).comp (X 0) h')

Goal state after:
Module: Mathlib.RepresentationTheory.Coinduced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : Semiring k
inst✝⁵ : Monoid G
inst✝⁴ : Monoid H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommMonoid A
inst✝² : Module k A
inst✝¹ : AddCommMonoid B
inst✝ : Module k B
σ : Representation k G A
ρ : Representation k G B
x✝¹ x✝ : H
⊢ (LinearMap.funLeft k B fun x ↦ x * (x✝¹ * x✝)).restrict ⋯ =
    (LinearMap.funLeft k B fun x ↦ x * x✝¹).restrict ⋯ * (LinearMap.funLeft k B fun x ↦ x * x✝).restrict ⋯

Tactic:
by ext; simp [mul_assoc]

Goal state after:
Module: Mathlib.RepresentationTheory.FinGroupCharZero

Goal state before:
pp: k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)

Tactic:
have := invertibleOfNonzero (NeZero.ne (Nat.card G : k))

Goal state after:
k : Type u
inst✝⁴ : Field k
G : Type u
inst✝³ : Group G
inst✝² : IsAlgClosed k
inst✝¹ : CharZero k
inst✝ : Fintype G
V : FDRep k G
this : Invertible ↑(Nat.card G)
⊢ Simple V ↔ ∑ g, V.character g * V.character g⁻¹ = ↑(Nat.card G)
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
H✝ : Type u_6
inst✝⁹ : Monoid H✝
π✝¹ : ContRepresentation R G✝ V
π' : ContRepresentation R H✝ W
G : Type u_7
H : Type u_8
inst✝⁸ : Group G
inst✝⁷ : TopologicalSpace G
inst✝⁶ : TopologicalSpace R
inst✝⁵ : ContinuousSMul R V
inst✝⁴ : ContinuousSMul R W
inst✝³ : Group H
inst✝² : TopologicalSpace H
φ : G →ₜ* H
π✝ : ContRepresentation R G V
inst✝¹ : IsTopologicalGroup G
inst✝ : IsTopologicalGroup H
π : ContRepresentation R G V
x✝¹ x✝ : G
⊢ { toFun := fun f ↦ (↑(π (x✝¹ * x✝))).comp (f.comp (ContinuousMap.mulLeft (x✝¹ * x✝)⁻¹)), map_add' := ⋯,
      map_smul' := ⋯, cont := ⋯ } =
    { toFun := fun f ↦ (↑(π x✝¹)).comp (f.comp (ContinuousMap.mulLeft x✝¹⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ } *
      { toFun := fun f ↦ (↑(π x✝)).comp (f.comp (ContinuousMap.mulLeft x✝⁻¹)), map_add' := ⋯, map_smul' := ⋯,
        cont := ⋯ }

Tactic:
by ext; simp [mul_assoc]

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

Goal state before:
pp: case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι -
      ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1)) =
    0

Tactic:
sub_eq_zero

Goal state after:
case succ
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
n : ℕ
ih : X.d n ≫ X.d (n + 1) = 0
⊢ X.d (n + 1) ≫ ofHom (X.resolutionX (n + 1 + 1)).ρ.coind₁ι =
    ofHom (X.resolutionX (n + 1)).ρ.coind₁ι ≫ (coind₁Functor k G).map (X.d (n + 1))
Module: Mathlib.RepresentationTheory.Homological.ContCohomology.LowDegree

Goal state before:
pp: k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ - (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ = 0
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1

Tactic:
sub_eq_zero

Goal state after:
k : Type u_1
G : Type u_2
inst✝⁴ : Ring k
inst✝³ : Group G
inst✝² : TopologicalSpace k
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
X : TopRep k G
σ : ↑(X.homogeneousCochains.X 0).toModuleCat
hσ : (X.resolutionX (0 + 1)).ρ.coind₁ι ↑σ = (Hom.hom ((coind₁Functor k G).map (ofHom X.ρ.coind₁ι))) ↑σ
g : G
⊢ (X.ρ g) (↑σ 1) = ↑σ 1
Module: Mathlib.RepresentationTheory.Induced

Goal state before:
pp: k : Type u_1
G : Type u_2
H : Type u_3
inst✝⁶ : CommRing k
inst✝⁵ : Group G
inst✝⁴ : Group H
φ : G →* H
A : Type u_4
B : Type u_5
inst✝³ : AddCommGroup A
inst✝² : Module k A
ρ : Representation k G A
inst✝¹ : AddCommGroup B
inst✝ : Module k B
τ : Representation k G B
h : H
x✝ : G
⊢ LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹) ∘ₗ
      (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ =
    (tprod (MonoidHom.comp (leftRegular k H) φ) ρ) x✝ ∘ₗ
      LinearMap.rTensor A (MonoidAlgebra.mapDomainLinearMap k k fun x ↦ x * h⁻¹)

Tactic:
by ext; simp [mul_assoc]

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
⊢ (forget₂ToModuleCatHomotopyEquiv k G).hom.f 0 = (forget₂ (Rep k G) (ModuleCat k)).map (ε k G)

Tactic:
refine ModuleCat.hom_ext <| MonoidAlgebra.lhom_ext' fun (x : Fin 1 → G) => LinearMap.ext_ring ?_
  simp [forget₂ToModuleCatHomotopyEquiv, HomotopyEquiv.ofIso, HomotopyEquiv.trans,
    SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv, ChainComplex.single₀_map_f_zero,
    AlgebraicTopology.AlternatingFaceMapComplex.ε_app_f_zero, compForgetAugmentedIso, eqToIso.inv,
    HomologicalComplex.eqToHom_f, compForgetAugmented, compForgetAugmented.toModule, ε,
    SimplicialObject.augment, Unique.eq_default (terminal.from _), MonoidAlgebra.coeff_single,
    Finsupp.single_apply, if_pos (Subsingleton.elim _ _)]

Goal state after:
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 : ℕ
⊢ d A (n + 1) ≫ d A n = 0

Tactic:
simpa [ChainComplex.of.d] using ((inhomogeneousChains A).d_comp_d (n + 2) (n + 1) n)

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

Goal state before:
pp: k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (x : G × G × G), (ModuleCat.Hom.hom (d₂₃ A)) f x = 0 x) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0

Tactic:
d₂₃_hom_apply,

Goal state after:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A : Rep k G
f : G × G → ↑A
⊢ (∀ (x : G × G × G), (A.ρ x.1) (f x.2) - f (x.1 * x.2.1, x.2.2) + f (x.1, x.2.1 * x.2.2) - f (x.1, x.2.1) = 0 x) ↔
    ∀ (g h j : G), (A.ρ g) (f (h, j)) - f (g * h, j) + f (g, h * j) - f (g, h) = 0
Module: Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality

Goal state before:
pp: k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : res f A ⟶ B
n✝ : ℕ
e : G ≃* H
e' : ↑B ≃ₗ[k] ↑A
he : ∀ (g : G), ↑e' ∘ₗ B.ρ g = A.ρ (e g) ∘ₗ ↑e'
n : ℕ
⊢ (Hom.hom
        ((resFunctor ↑e).map (ofHom { toLinearMap := ↑e', isIntertwining' := ⋯ }) ≫
          ofHom { toLinearMap := ↑e'.symm, isIntertwining' := ⋯ })).toLinearMap =
    (Hom.hom (𝟙 B)).toLinearMap

Tactic:
by simp [res_id]

Goal state after: