mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X Y : Action (Type w) G
f : X ⟶ Y
x : X.V
r : k
⊢ (linearizeMap f) (MonoidAlgebra.single x r) = MonoidAlgebra.single ((ConcreteCategory.hom f.hom) x) r

Tactic:
by

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (a : Ω), (Y j ^ 2) a = ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ

Tactic:
by

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.{w + 1}).symm ∘ₗ (trivial k G k) g =
    (linearize k G (𝟙_ (Action (Type w) G))) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k PUnit.{w + 1}).symm

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
⊢ (ε k G) 1 = MonoidAlgebra.single PUnit.unit 1

Tactic:
by

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:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
x : PUnit.{u + 1}
⊢ (η k G) (MonoidAlgebra.single x 1) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
⊢ (ε k G).comp (η k G) = IntertwiningMap.id (linearize k G (𝟙_ (Action (Type u) G)))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
⊢ (η k G).comp (ε k G) = IntertwiningMap.id (trivial k G k)

Tactic:
by

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∫ (x : ℝ) in 0..↑j, x ^ 2 ∂ρ =
    ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
by

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
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ ↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g =
    (linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
r s : k
⊢ (μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
l1 : k[X.V]
l2 : k[Y.V]
xy : (X ⊗ Y).V
⊢ ((μ X Y) (l1 ⊗ₜ[k] l2)).coeff xy = l1.coeff xy.1 * l2.coeff xy.2

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ (μ Y Z).comp (rTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (f ▷ Z)).comp (μ X Z)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
⊢ (μ Z Y).comp (lTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (Z ◁ f)).comp (μ Z X)

Tactic:
by

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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ ∫ (x : Ω), rexp (↑q * X x) * ∫ (y : Ω''), rexp (↑q * Y y) ∂η (ω', x) ∂κ ω' ≤
    ∫ (x : Ω), rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2) ∂κ ω'

Tactic:
by

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ j ∈ range K, (↑j ^ 2)⁻¹ * ∑ k ∈ range j, ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ =
    ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ((linearizeMap (α_ X Y Z).hom).comp (μ (X ⊗ Y) Z)).comp (rTensor (linearize k G Z) (μ X Y)) =
    ((μ X (Y ⊗ Z)).comp (lTensor (linearize k G X) (μ Y Z))).comp
      ↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ↑(lid k (linearize k G X)) =
    ((linearizeMap (λ_ X).hom).comp (μ (𝟙_ (Action (Type w) G)) X)).comp (rTensor (linearize k G X) (ε k G))

Tactic:
by

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, (∑ j ∈ Ioo k K, (↑j ^ 2)⁻¹) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤
    ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ↑(rid k (linearize k G X)) =
    ((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp (lTensor (linearize k G X) (ε k G))

Tactic:
by

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 : ℕ
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
⊢ ↑k ≤ ↑(k + 1)

Tactic:
by

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
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
⊢ ↑(MonoidAlgebra.tensorEquiv k).symm ∘ₗ (linearize k G (X ⊗ Y)) g =
    ((linearize k G X).tprod (linearize k G Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k).symm

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
xy : (X ⊗ Y).V
⊢ (δ X Y) (MonoidAlgebra.single xy 1) = MonoidAlgebra.single xy.1 1 ⊗ₜ[k] MonoidAlgebra.single xy.2 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
⊢ (rTensor (linearize k G Z) (linearizeMap f)).comp (δ X Z) = (δ Y Z).comp (linearizeMap (f ▷ Z))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
⊢ (lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X) = (δ Z Y).comp (linearizeMap (Z ◁ f))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ ((↑(assoc (linearize k G X) (linearize k G Y) (linearize k G Z))).comp (rTensor (linearize k G Z) (δ X Y))).comp
      (δ (X ⊗ Y) Z) =
    ((lTensor (linearize k G X) (δ Y Z)).comp (δ X (Y ⊗ Z))).comp (linearizeMap (α_ X Y Z).hom)

Tactic:
by

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 : ℕ
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)
⊢ Continuous fun x ↦ 2 / (↑k + 1) * x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
⊢ ↑(lid k (linearize k G X)).symm =
    ((rTensor (linearize k G X) (η k G)).comp (δ (𝟙_ (Action (Type u) G)) X)).comp (linearizeMap (λ_ X).inv)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
⊢ ↑(rid k (linearize k G X)).symm =
    ((lTensor (linearize k G X) (η k G)).comp (δ X (𝟙_ (Action (Type u) G)))).comp (linearizeMap (ρ_ X).inv)

Tactic:
by

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 : ℕ
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)
⊢ Continuous (HMul.hMul 2)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ (μ X Y).comp (δ X Y) = IntertwiningMap.id (linearize k G (X ⊗ Y))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
⊢ (δ X Y).comp (μ X Y) = IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))

Tactic:
by

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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
hκ : IsSFiniteKernel κ
q : ℚ
ω' : Ω'
hX_mgf : ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)
hX_int : Integrable (fun y ↦ rexp (↑q * X y)) (κ ω')
hY_mgf : ∀ᵐ (b : Ω) ∂κ ω', ∀ (t : ℝ), mgf Y (η (ω', b)) t ≤ rexp (↑cY * t ^ 2 / 2)
h_int_mul : Integrable (fun ω ↦ rexp (↑q * (X ω.1 + Y ω.2))) ((κ ⊗ₖ η) ω')
⊢ ∫ (x : Ω), rexp (↑q * X x) * rexp (↑cY * ↑q ^ 2 / 2) ∂κ ω' ≤ rexp (↑(c + cY) * ↑q ^ 2 / 2)

Tactic:
by

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 : ℕ
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 = x / (↑k + 1) * (2 * x)

Tactic:
by

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
Ω'' : Type u_3
mΩ'' : MeasurableSpace Ω''
Y : Ω'' → ℝ
cY : ℝ≥0
inst✝¹ : SFinite ν
η : Kernel (Ω' × Ω) Ω''
inst✝ : IsZeroOrMarkovKernel η
hX : HasSubgaussianMGF X c κ ν
hY : HasSubgaussianMGF Y cY η (ν ⊗ₘ κ)
⊢ HasSubgaussianMGF (fun p ↦ X p.1 + Y p.2) (c + cY) (κ ⊗ₖ η) ν

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Type w
g : G
⊢ (linearize k G (Action.trivial G X)) g = LinearMap.id

Tactic:
by

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 : ℕ
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)
this : 0 < x
⊢ 0 < ↑k + 1

Tactic:
by

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 : ℕ
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)
⊢ x / (↑k + 1) * (2 * x) ≤ 1 * (2 * x)

Tactic:
by

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
X : Type w
g : G
⊢ ↑(LinearEquiv.refl k k[(Action.trivial G X).V]) ∘ₗ (linearize k G (Action.trivial G X)) g =
    (trivial k G k[X]) g ∘ₗ ↑(LinearEquiv.refl k k[(Action.trivial G X).V])

Tactic:
by

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 : ℕ
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)
⊢ 1 * (2 * x) = 2 * x

Tactic:
by

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝⁹ : Field k
inst✝⁸ : Ring A
inst✝⁷ : Algebra k A
inst✝⁶ : AddCommGroup V
inst✝⁵ : Module k V
inst✝⁴ : Module A V
inst✝³ : IsScalarTower k A V
inst✝² : IsSimpleModule A V
inst✝¹ : FiniteDimensional k V
inst✝ : IsAlgClosed k
⊢ Function.Bijective ⇑(algebraMap k (Module.End A V))

Tactic:
by

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
this : Nontrivial V
v : V
v_nz : v ≠ 0
a : A
w : V
hw : w ∈ (k ∙ v).carrier
⊢ a • w ∈ (k ∙ v).carrier

Tactic:
by

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 : ℕ
Y : ℕ → Ω → ℝ := fun n ↦ truncation X ↑n
ρ : Measure ℝ := Measure.map X ℙ
Y2 : ∀ (n : ℕ), ∫ (a : Ω), (Y n ^ 2) a = ∫ (x : ℝ) in 0..↑n, x ^ 2 ∂ρ
⊢ ∑ k ∈ range K, 2 / (↑k + 1) * ∫ (x : ℝ) in ↑k..↑(k + 1), x ^ 2 ∂ρ ≤ ∑ k ∈ range K, ∫ (x : ℝ) in ↑k..↑(k + 1), 2 * x ∂ρ

Tactic:
by

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

Goal state before:
pp: A : Type u_1
V : Type u_2
k : Type u_3
inst✝¹⁰ : Field k
inst✝⁹ : Ring A
inst✝⁸ : Algebra k A
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
inst✝⁵ : Module A V
inst✝⁴ : IsScalarTower k A V
inst✝³ : IsSimpleModule A V
inst✝² : FiniteDimensional k V
inst✝¹ : IsAlgClosed k
inst✝ : IsMulCommutative A
⊢ Module.finrank k V = 1

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝⁸ : Semiring k
G : Type v
inst✝⁷ : Monoid G
V : Type v'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module k V
W : Type w'
inst✝⁴ : AddCommMonoid W
inst✝³ : Module k W
H : Type w
inst✝² : Subsingleton H
inst✝¹ : MulOneClass H
inst✝ : MulAction G H
g : G
⊢ ↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g =
    (trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝⁸ : Semiring k
G : Type v
inst✝⁷ : Monoid G
V : Type v'
inst✝⁶ : AddCommMonoid V
inst✝⁵ : Module k V
W : Type w'
inst✝⁴ : AddCommMonoid W
inst✝³ : Module k W
H : Type w
inst✝² : Subsingleton H
inst✝¹ : MulOneClass H
inst✝ : MulAction G H
g : G
⊢ ↑(MonoidAlgebra.mapDomainLinearEquiv k k (Equiv.funUnique (Fin 1) G)) ∘ₗ (diagonal k G 1) g =
    (leftRegular k G) g ∘ₗ ↑(MonoidAlgebra.mapDomainLinearEquiv k k (Equiv.funUnique (Fin 1) G))

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : Monoid G
f : Fin 1 → G
r : k
⊢ (diagonalOneEquivLeftRegular k G) (MonoidAlgebra.single f r) = MonoidAlgebra.single (f 0) r

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k : Type u
inst✝¹ : Semiring k
G : Type v
inst✝ : Monoid G
g : G
r : k
⊢ (diagonalOneEquivLeftRegular k G).symm (MonoidAlgebra.single g r) = MonoidAlgebra.single (uniqueElim g) r

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
g : G
⊢ ((linearCombination k fun x ↦ (σ x.2) (f x.1)) ∘ₗ
        ↑(curryLinearEquiv k).symm ∘ₗ mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
      (free k G α) g =
    σ g ∘ₗ
      (linearCombination k fun x ↦ (σ x.2) (f x.1)) ∘ₗ
        ↑(curryLinearEquiv k).symm ∘ₗ mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝³ : Monoid G
V : Type v'
inst✝² : AddCommMonoid V
k : Type u
inst✝¹ : CommSemiring k
inst✝ : Module k V
σ : Representation k G V
α : Type w'
i : α
g : G
r : k
f : α → V
⊢ (σ.freeLift f) (single i (MonoidAlgebra.single g r)) = r • (σ g) (f i)

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
m mΩ : MeasurableSpace Ω
hm : m ≤ mΩ
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
X : Ω → ℝ
c : ℝ≥0
h : HasCondSubgaussianMGF m hm X c μ
t : ℝ
⊢ ∀ᵐ (ω' : Ω) ∂μ.trim hm, μ[fun ω ↦ rexp (t * X ω) | m] ω' ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : (free k G α).IntertwiningMap σ
⊢ σ.freeLift ((fun f i ↦ f (single i (MonoidAlgebra.single 1 1))) f) = f

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹¹ : Semiring k✝
G : Type v
inst✝¹⁰ : Monoid G
V : Type v'
inst✝⁹ : AddCommMonoid V
inst✝⁸ : Module k✝ V
W : Type w'
inst✝⁷ : AddCommMonoid W
inst✝⁶ : Module k✝ W
H : Type w
inst✝⁵ : Subsingleton H
inst✝⁴ : MulOneClass H
inst✝³ : MulAction G H
k : Type u
inst✝² : CommSemiring k
inst✝¹ : Module k V
inst✝ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
f : α → V
⊢ (fun f i ↦ f (single i (MonoidAlgebra.single 1 1))) (σ.freeLift f) = f

Tactic:
by

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

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
x✝ : HasSubgaussianMGF X c μ
h1 : ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) μ
h2 : ∀ (t : ℝ), mgf X μ t ≤ rexp (↑c * t ^ 2 / 2)
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑(Kernel.const Unit μ) ∘ₘ Measure.dirac ())

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: k✝ : Type u
inst✝¹² : Semiring k✝
G : Type v
inst✝¹¹ : Monoid G
V : Type v'
inst✝¹⁰ : AddCommMonoid V
inst✝⁹ : Module k✝ V
W : Type w'
inst✝⁸ : AddCommMonoid W
inst✝⁷ : Module k✝ W
H : Type w
inst✝⁶ : Subsingleton H
inst✝⁵ : MulOneClass H
inst✝⁴ : MulAction G H
k : Type u
inst✝³ : CommSemiring k
inst✝² : Module k V
inst✝¹ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst✝ : DecidableEq α
g : G
⊢ ↑(TensorProduct.finsuppLeft k k V W α) ∘ₗ ((σ.finsupp α).tprod ρ) g =
    ((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppLeft k k V W α)

Tactic:
by

Goal state after:
Module: Mathlib.RepresentationTheory.Equiv

Goal state before:
pp: G : Type v
inst✝⁶ : Monoid G
V : Type v'
inst✝⁵ : AddCommMonoid V
W : Type w'
inst✝⁴ : AddCommMonoid W
k : Type u
inst✝³ : CommSemiring k
inst✝² : Module k V
inst✝¹ : Module k W
σ : Representation k G V
ρ : Representation k G W
α : Type w'
inst✝ : DecidableEq α
f : α →₀ V
w : W
⊢ (σ.finsuppTensorLeft ρ α) (f ⊗ₜ[k] w) = f.sum fun i v ↦ single i (v ⊗ₜ[k] w)

Tactic:
by

Goal state after: