mathlib-initiative/mathlib-tactics huggingface dataset:
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:
;

Goal state after:
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✝
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:
;

Goal state after:
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✝
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:
;

Goal state after:
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✝
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 (↑(rid k (linearize k G X))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x) 1)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry
                (((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp
                    (lTensor (linearize k G X) (ε k G))).toLinearMap ∘ₗ
              MonoidAlgebra.lsingle x)
            1)
          1).coeff
      a✝

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x a✝ : X.V
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(rid k (linearize k G X))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x) 1)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry
                (((linearizeMap (ρ_ X).hom).comp (μ X (𝟙_ (Action (Type w) G)))).comp
                    (lTensor (linearize k G X) (ε k G))).toLinearMap ∘ₗ
              MonoidAlgebra.lsingle x)
            1)
          1).coeff
      a✝
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
x✝ : (X ⊗ Y).V
⊢ ((↑(MonoidAlgebra.tensorEquiv k).symm ∘ₗ (linearize k G (X ⊗ Y)) g) ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((linearize k G X).tprod (linearize k G Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k).symm) ∘ₗ MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
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
x✝ : (X ⊗ Y).V
⊢ ((↑(MonoidAlgebra.tensorEquiv k).symm ∘ₗ (linearize k G (X ⊗ Y)) g) ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((linearize k G X).tprod (linearize k G Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k).symm) ∘ₗ MonoidAlgebra.lsingle x✝)
      1
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
x✝ : (X ⊗ Y).V
⊢ MonoidAlgebra.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) x✝).1 1 ⊗ₜ[k]
      MonoidAlgebra.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) x✝).2 1 =
    MonoidAlgebra.single ((ConcreteCategory.hom (X.ρ g)) x✝.1) 1 ⊗ₜ[k]
      MonoidAlgebra.single ((ConcreteCategory.hom (Y.ρ g)) x✝.2) 1

Tactic:
;

Goal state after:
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
x✝ : (X ⊗ Y).V
⊢ MonoidAlgebra.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) x✝).1 1 ⊗ₜ[k]
      MonoidAlgebra.single ((ConcreteCategory.hom ((X ⊗ Y).ρ g)) x✝).2 1 =
    MonoidAlgebra.single ((ConcreteCategory.hom (X.ρ g)) x✝.1) 1 ⊗ₜ[k]
      MonoidAlgebra.single ((ConcreteCategory.hom (Y.ρ g)) x✝.2) 1
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
x✝ : (X ⊗ Z).V
⊢ (((rTensor (linearize k G Z) (linearizeMap f)).comp (δ X Z)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Y Z).comp (linearizeMap (f ▷ Z))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
x✝ : (X ⊗ Z).V
⊢ (((rTensor (linearize k G Z) (linearizeMap f)).comp (δ X Z)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Y Z).comp (linearizeMap (f ▷ Z))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1
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
x✝ : (Z ⊗ X).V
⊢ (((lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Z Y).comp (linearizeMap (Z ◁ f))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
f : X ⟶ Y
x✝ : (Z ⊗ X).V
⊢ (((lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    (((δ Z Y).comp (linearizeMap (Z ◁ f))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1
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
x✝ : X.V
⊢ ((↑(rid k (linearize k G X)).symm).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((lTensor (linearize k G X) (η k G)).comp (δ X (𝟙_ (Action (Type u) G)))).comp
            (linearizeMap (ρ_ X).inv)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
x✝ : X.V
⊢ ((↑(rid k (linearize k G X)).symm).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((lTensor (linearize k G X) (η k G)).comp (δ X (𝟙_ (Action (Type u) G)))).comp
            (linearizeMap (ρ_ X).inv)).toLinearMap ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
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✝ a✝ : (X ⊗ Y).V
⊢ ((((μ X Y).comp (δ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (X ⊗ Y))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x✝ a✝ : (X ⊗ Y).V
⊢ ((((μ X Y).comp (δ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝ =
    (((IntertwiningMap.id (linearize k G (X ⊗ Y))).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1).coeff a✝
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
x✝ : Y.V
⊢ ((TensorProduct.AlgebraTensorModule.curry ((δ X Y).comp (μ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝¹) 1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
              (IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))).toLinearMap ∘ₗ
            MonoidAlgebra.lsingle x✝¹)
          1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1

Tactic:
;

Goal state after:
G : Type v
inst✝¹ : Monoid G
X Y : Action (Type w) G
k : Type u
inst✝ : CommSemiring k
x✝¹ : X.V
x✝ : Y.V
⊢ ((TensorProduct.AlgebraTensorModule.curry ((δ X Y).comp (μ X Y)).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝¹) 1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((TensorProduct.AlgebraTensorModule.curry
              (IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))).toLinearMap ∘ₗ
            MonoidAlgebra.lsingle x✝¹)
          1 ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1
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
a : H
⊢ ((↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g) ∘ₗ MonoidAlgebra.lsingle a) 1 =
    (((trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)) ∘ₗ MonoidAlgebra.lsingle a) 1

Tactic:
;

Goal state after:
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
a : H
⊢ ((↑(MonoidAlgebra.uniqueLinearEquiv k H) ∘ₗ (ofMulAction k G H) g) ∘ₗ MonoidAlgebra.lsingle a) 1 =
    (((trivial k G k) g ∘ₗ ↑(MonoidAlgebra.uniqueLinearEquiv k H)) ∘ₗ MonoidAlgebra.lsingle a) 1
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:
;

Goal state after:
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✝
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:
;

Goal state after:
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
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 : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 1)

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 ∂ρ
⊢ ∫ (x : ℝ) in ↑0..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0..↑K, x ∂ρ

Tactic:
;

Goal state after:
Ω : 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 : ℕ
x✝ : k < K
⊢ IntervalIntegrable (HMul.hMul 2) ρ ↑k ↑(k + 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 ∂ρ
⊢ ∫ (x : ℝ) in ↑0..↑K, 2 * x ∂ρ = 2 * ∫ (x : ℝ) in 0..↑K, x ∂ρ
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 σ
a✝ : α
x✝ : G
⊢ (((σ.freeLift ((fun f i ↦ f (single i (MonoidAlgebra.single 1 1))) f)).toLinearMap ∘ₗ lsingle a✝) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((f.toLinearMap ∘ₗ lsingle a✝) ∘ₗ MonoidAlgebra.lsingle x✝) 1

Tactic:
;

Goal state after:
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 σ
a✝ : α
x✝ : G
⊢ (((σ.freeLift ((fun f i ↦ f (single i (MonoidAlgebra.single 1 1))) f)).toLinearMap ∘ₗ lsingle a✝) ∘ₗ
        MonoidAlgebra.lsingle x✝)
      1 =
    ((f.toLinearMap ∘ₗ lsingle a✝) ∘ₗ MonoidAlgebra.lsingle x✝) 1
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
a✝¹ : α
x✝¹ : V
x✝ : W
a✝ : α
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(TensorProduct.finsuppLeft k k V W α) ∘ₗ ((σ.finsupp α).tprod ρ) g) ∘ₗ
            lsingle a✝¹)
          x✝¹)
        x✝)
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry (((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppLeft k k V W α)) ∘ₗ
            lsingle a✝¹)
          x✝¹)
        x✝)
      a✝

Tactic:
;

Goal state after:
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
a✝¹ : α
x✝¹ : V
x✝ : W
a✝ : α
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(TensorProduct.finsuppLeft k k V W α) ∘ₗ ((σ.finsupp α).tprod ρ) g) ∘ₗ
            lsingle a✝¹)
          x✝¹)
        x✝)
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry (((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppLeft k k V W α)) ∘ₗ
            lsingle a✝¹)
          x✝¹)
        x✝)
      a✝
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
x✝¹ : V
a✝¹ : α
x✝ : W
a✝ : α
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(TensorProduct.finsuppRight k k V W α) ∘ₗ (σ.tprod (ρ.finsupp α)) g))
            x✝¹ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry (((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppRight k k V W α)))
            x✝¹ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝

Tactic:
;

Goal state after:
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
x✝¹ : V
a✝¹ : α
x✝ : W
a✝ : α
⊢ (((TensorProduct.AlgebraTensorModule.curry (↑(TensorProduct.finsuppRight k k V W α) ∘ₗ (σ.tprod (ρ.finsupp α)) g))
            x✝¹ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry (((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppRight k k V W α)))
            x✝¹ ∘ₗ
          lsingle a✝¹)
        x✝)
      a✝
Module: Mathlib.Probability.Moments.SubGaussian

Goal state before:
pp: Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
X : Ω → ℝ
c : ℝ≥0
h : HasSubgaussianMGF X c μ
t : ℝ
p : ℝ≥0
⊢ MemLp (fun ω ↦ rexp (t * X ω)) (↑p) μ

Tactic:
rw [HasSubgaussianMGF_iff_kernel] at h
  simpa using h.memLp_exp_mul t p

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

Goal state after:
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