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

Goal state before:
pp: case e'_3
Ω : Type u_1
S : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
E : S → Type u_4
inst✝⁵ : (s : S) → TopologicalSpace (E s)
inst✝⁴ : (s : S) → MeasurableSpace (E s)
inst✝³ : ∀ (s : S), BorelSpace (E s)
inst✝² : ∀ (s : S), HasOuterApproxClosed (E s)
X : (s : S) → Ω → E s
inst✝¹ : IsProbabilityMeasure P
inst✝ : Finite S
A : Set Ω
mA : NullMeasurableSet A P
mX : ∀ (s : S), AEMeasurable (X s) P
h : ∀ (f : ((s : S) → E s) →ᵇ ℝ), ∫ (ω : Ω) in A, f fun x ↦ X x ω ∂P = P.real A * ∫ (ω : Ω), f fun x ↦ X x ω ∂P
this : Fintype S
f : (s : S) → E s →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (X s x✝) = (∏ s, (f s).compContinuous { toFun := Function.eval s, continuous_toFun := ⋯ }) fun x ↦ X x x✝

Tactic:
simp

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

Goal state before:
pp: case e'_2
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

Tactic:
simp

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

Goal state before:
pp: case e'_3
Ω : Type u_1
mΩ : MeasurableSpace Ω
P : Measure Ω
G : Type u_6
inst✝⁴ : TopologicalSpace G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : HasOuterApproxClosed G
Z : Ω → G
inst✝ : IsProbabilityMeasure P
A : Set Ω
mA : NullMeasurableSet A P
mZ : AEMeasurable Z P
h : ∀ (f : G →ᵇ ℝ), ∫ (ω : Ω) in A, f (Z ω) ∂P = P.real A * ∫ (ω : Ω), f (Z ω) ∂P
f : Unit → G →ᵇ ℝ
x✝ : Ω
⊢ ∏ s, (f s) (Z x✝) = (f ()) (Z x✝)

Tactic:
simp

Goal state after:
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
⊢ ∀ (t : T), X t =ᵐ[P] X t

Tactic:
simp

Goal state after:
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 : ℝ
P : Measure Ω
X : T → Ω → E
hX : IsAEKolmogorovProcess X P p q 0
s t : T
⊢ 0 * edist s t ^ q = 0

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsZeroOrMarkovKernel κ
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * 0)) (⇑κ ∘ₘ ν)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
ν : Measure Ω'
κ : Kernel Ω' Ω
inst✝¹ : IsFiniteMeasure ν
inst✝ : IsZeroOrMarkovKernel κ
⊢ ∀ᵐ (ω' : Ω') ∂ν, ∀ (t : ℝ), mgf (fun x ↦ 0) (κ ω') t ≤ rexp (↑0 * t ^ 2 / 2)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ (t : ℝ), Integrable (fun ω ↦ rexp (t * X ω)) (⇑κ ∘ₘ 0)

Tactic:
simp

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

Goal state before:
pp: Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
κ : Kernel Ω' Ω
X : Ω → ℝ
c : ℝ≥0
⊢ ∀ᵐ (ω' : Ω') ∂0, ∀ (t : ℝ), mgf X (κ ω') t ≤ rexp (↑c * t ^ 2 / 2)

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
inst✝² : Preorder ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
𝓕 : Filtration ι mΩ
P : Measure Ω
x✝³ : Ω
x✝² x✝¹ : ℕ
x✝ : x✝² ≤ x✝¹
⊢ (fun x ↦ ⊤) x✝² ≤ (fun x ↦ ⊤) x✝¹

Tactic:
simp

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✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ 1).restrict ⋯) x✝) = ↑(1 x✝)

Tactic:
simp

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✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
ρ' : Subrepresentation ρ
x y : G
x✝ : ↥ρ'.toSubmodule
⊢ ↑(((ρ (x * y)).restrict ⋯) x✝) = ↑(((ρ x).restrict ⋯ * (ρ y).restrict ⋯) x✝)

Tactic:
simp

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✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ⊤ → (ρ g) v ∈ ⊤

Tactic:
simp

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✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid W
inst✝² : Module A W
ρ : Representation A G W
inst✝¹ : AddCommMonoid M
inst✝ : Module A[G] M
⊢ ∀ (g : G) ⦃v : W⦄, v ∈ ⊥ → (ρ g) v ∈ ⊥

Tactic:
simp

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
⊢ MonoidAlgebra.single g a • v ∈ σ.toSubmodule.carrier

Tactic:
Representation.single_smul

Goal state after:
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
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁴ : ConditionallyCompleteLinearOrderBot ι
inst✝³ : TopologicalSpace ι
inst✝² : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝¹ : SecondCountableTopology ι
inst✝ : IsFiniteMeasure P
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
T : ℕ → ι
hT : Tendsto T atTop atTop
n : ℕ
hn : ∀ (k : ℕ), (1 / 2) ^ n < P {ω | σ n k ω < min (τ n ω) ↑(T n)}
this : (1 / 2) ^ n ≤ P (⋂ k, {ω | σ n k ω < min (τ n ω) ↑(T n)})
⊢ ¬(1 / 2) ^ n ≤ 0

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |truncation f A x| ≤ |f x|

Tactic:
simp only [truncation, indicator, id, Function.comp_apply]

Goal state after:
α : Type u_1
f : α → ℝ
A : ℝ
x : α
⊢ |if f x ∈ Set.Ioc (-A) A then f x else 0| ≤ |f x|
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
⊢ 1 / 2 < 1

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case h.hf
Ω : Type u_1
inst✝¹ : MeasureSpace Ω
inst✝ : IsProbabilityMeasure ℙ
X : Ω → ℝ
hint : Integrable X ℙ
hnonneg : 0 ≤ X
K N : ℕ
hKN : K ≤ N
ρ : Measure ℝ := ⋯
this : IsProbabilityMeasure ρ
i : ℕ
a✝ : i ∈ range N
⊢ ∀ u ∈ Set.Icc (↑i) (↑i + 1), 0 ≤ 1

Tactic:
· simp only [zero_le_one, imp_true_iff]

Goal state after:
Module: Mathlib.Probability.Process.LocalProperty

Goal state before:
pp: ι : Type u_1
Ω : Type u_2
mΩ : MeasurableSpace Ω
P : Measure Ω
inst✝⁵ : ConditionallyCompleteLinearOrderBot ι
inst✝⁴ : TopologicalSpace ι
inst✝³ : OrderTopology ι
𝓕 : Filtration ι mΩ
inst✝² : SecondCountableTopology ι
inst✝¹ : IsFiniteMeasure P
inst✝ : NoMaxOrder ι
τ : ℕ → Ω → WithTop ι
σ : ℕ → ℕ → Ω → WithTop ι
hτ : IsLocalizingSequence 𝓕 τ P
hσ : ∀ (n : ℕ), IsLocalizingSequence 𝓕 (σ n) P
nk : ℕ → ℕ
T : ℕ → ι
hnk : StrictMono nk
hT : Tendsto T atTop atTop
hP : ∀ (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} ≤ (1 / 2) ^ n
this : ∑' (n : ℕ), P {ω | σ n (nk n) ω < min (τ n ω) ↑(T n)} < ∞
ω : Ω
hω : ∀ᶠ (n : ℕ) in atTop, ¬σ n (nk n) ω < min (τ n ω) ↑(T n)
hωτ : Tendsto (fun x ↦ τ x ω) atTop (𝓝 ⊤)
⊢ ∀ᶠ (b : ℕ) in atTop, σ b (nk b) ω ≤ min ⊤ ⊤

Tactic:
simp

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✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ 1)) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    ((1 ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
simp

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✝² x✝¹ : G
x✝ a✝ : X.V
⊢ ((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ (x✝² * x✝¹))) ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff
      a✝ =
    (((MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝²)) *
              MonoidAlgebra.mapDomainLinearMap k k ⇑(ConcreteCategory.hom (X.ρ x✝¹))) ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
X : Action (Type w) G
g : G
x : X.V
⊢ ((linearize k G X) g) (MonoidAlgebra.single x 1) = MonoidAlgebra.single ((ConcreteCategory.hom (X.ρ g)) x) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: k : Type u
G : Type v
inst✝¹ : Monoid G
inst✝ : Semiring k
x✝ : (𝟙_ (Action (Type u) G)).V
a✝ : (𝟙_ (Action (Type u) G)).V
⊢ ((((ε k G).comp (η k G)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (𝟙_ (Action (Type u) G)))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
simp

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)).toLinearMap 1 = (IntertwiningMap.id (trivial k G k)).toLinearMap 1

Tactic:
simp

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
x✝¹ : X.V
x✝ : Z.V
a✝ : (Y ⊗ Z).V
⊢ (((TensorProduct.AlgebraTensorModule.curry ((μ Y Z).comp (rTensor (linearize k G Z) (linearizeMap f))).toLinearMap ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((linearizeMap (f ▷ Z)).comp (μ X Z)).toLinearMap ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
simp

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
x✝¹ : Z.V
x✝ : X.V
a✝ : (Z ⊗ Y).V
⊢ (((TensorProduct.AlgebraTensorModule.curry ((μ Z Y).comp (lTensor (linearize k G Z) (linearizeMap f))).toLinearMap ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((linearizeMap (Z ◁ f)).comp (μ Z X)).toLinearMap ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: case e'_2
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle y) 1) ⊗ₜ[k]
        (MonoidAlgebra.lsingle z) 1) =
    MonoidAlgebra.single ((x, y), z) 1

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Action

Goal state before:
pp: case e'_3
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ (MonoidAlgebra.tensorEquiv k)
      ((MonoidAlgebra.lsingle x) 1 ⊗ₜ[k]
        (MonoidAlgebra.tensorEquiv k) ((MonoidAlgebra.lsingle y) 1 ⊗ₜ[k] (MonoidAlgebra.lsingle z) 1)) =
    MonoidAlgebra.single ((ConcreteCategory.hom (α_ X Y Z).hom.hom) ((x, y), z)) 1

Tactic:
simp

Goal state after:
Module: Mathlib.Probability.StrongLaw

Goal state before:
pp: case ha
Ω : 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:
simp

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
x✝ a✝ : X.V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(lid k (linearize k G X))).toLinearMap) 1 ∘ₗ MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry
                (((linearizeMap (λ_ X).hom).comp (μ (𝟙_ (Action (Type w) G)) X)).comp
                    (rTensor (linearize k G X) (ε k G))).toLinearMap)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
simp

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

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
x✝ : Fin 1 → G
a✝ : G
⊢ (((↑(MonoidAlgebra.mapDomainLinearEquiv k k (Equiv.funUnique (Fin 1) G)) ∘ₗ (diagonal k G 1) g) ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    ((((leftRegular k G) g ∘ₗ ↑(MonoidAlgebra.mapDomainLinearEquiv k k (Equiv.funUnique (Fin 1) G))) ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝

Tactic:
simp

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
a✝ : α
x✝ : G
⊢ (((((linearCombination k fun x ↦ (σ x.2) (f x.1)) ∘ₗ
              ↑(curryLinearEquiv k).symm ∘ₗ mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
            (free k G α) g) ∘ₗ
          lsingle a✝) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    (((σ g ∘ₗ
            (linearCombination k fun x ↦ (σ x.2) (f x.1)) ∘ₗ
              ↑(curryLinearEquiv k).symm ∘ₗ mapRange.linearMap ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
          lsingle a✝) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
simp

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'
g x✝¹ : G
x✝ a✝¹ : α
a✝ : G
⊢ ((((TensorProduct.AlgebraTensorModule.curry
                    (↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm) ∘ₗ
                      ((leftRegular k G).tprod (trivial k G k[α])) g) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝ =
    ((((TensorProduct.AlgebraTensorModule.curry
                    ((free k G α) g ∘ₗ
                      ↑(TensorProduct.congr (MonoidAlgebra.coeffLinearEquiv k) (MonoidAlgebra.coeffLinearEquiv k) ≪≫ₗ
                                finsuppTensorFinsupp' k G α ≪≫ₗ
                              Finsupp.domLCongr (Equiv.prodComm G α) ≪≫ₗ
                            curryLinearEquiv k ≪≫ₗ
                          mapRange.linearEquiv (MonoidAlgebra.coeffLinearEquiv k).symm)) ∘ₗ
                  MonoidAlgebra.lsingle x✝¹)
                1 ∘ₗ
              MonoidAlgebra.lsingle x✝)
            1)
          a✝¹).coeff
      a✝

Tactic:
simp

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
v : V
g g' : G
⊢ (((((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ (leftRegular k G) g) ∘ₗ
        MonoidAlgebra.lsingle g')
      1 =
    ((σ g ∘ₗ ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k)) ∘ₗ
        MonoidAlgebra.lsingle g')
      1

Tactic:
simp

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
v : V
⊢ (fun f ↦ (Finsupp.llift V k k G).symm (f.toLinearMap ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k).symm) 1)
      ((fun v ↦
          { toLinearMap := ((Finsupp.llift V k k G) fun g ↦ (σ g) v) ∘ₗ ↑(MonoidAlgebra.coeffLinearEquiv k),
            isIntertwining' := ⋯ })
        v) =
    v

Tactic:
simp

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
g : G
v : V
⊢ (σ.leftRegularMapEquiv.symm v) (MonoidAlgebra.single g 1) = (σ g) v

Tactic:
simp

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

Goal state before:
pp: case empty
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
X : ι → Ω → ℝ
h_indep : iIndepFun X μ
c : ι → ℝ≥0
h_meas : ∀ (i : ι), AEMeasurable (X i) μ
this : IsProbabilityMeasure μ
h_subG : ∀ i ∈ ∅, HasSubgaussianMGF (X i) (c i) μ
⊢ HasSubgaussianMGF (fun ω ↦ ∑ i ∈ ∅, X i ω) (∑ i ∈ ∅, c i) μ

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
by
  intro f g h
  ext x
  exact congrFun h x

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

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

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

Goal state before:
pp: case empty
A : Type u_1
G : Type u_2
V : Type u_3
W : Type u_4
inst✝⁵ : Semiring A
inst✝⁴ : Monoid G
inst✝³ : AddCommMonoid V
inst✝² : AddCommMonoid W
inst✝¹ : Module A V
inst✝ : Module A W
ρ : Representation A G V
σ : Representation A G W
ι : Type u_6
f : ι → ρ.IntertwiningMap σ
⊢ (∑ i ∈ ∅, f i).toLinearMap = ∑ i ∈ ∅, (f i).toLinearMap

Tactic:
simp

Goal state after:
Module: Mathlib.RepresentationTheory.Intertwining

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

Tactic:
simp

Goal state after: