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
⊢ (η k G).comp (ε k G) = IntertwiningMap.id (trivial k G k)

Tactic:
ext

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

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.V
x✝ : Y.V
a✝ : (X ⊗ Y).V
⊢ (((TensorProduct.AlgebraTensorModule.curry
                  (↑(MonoidAlgebra.tensorEquiv k) ∘ₗ ((linearize k G X).tprod (linearize k G Y)) g) ∘ₗ
                MonoidAlgebra.lsingle x✝¹)
              1 ∘ₗ
            MonoidAlgebra.lsingle x✝)
          1).coeff
      a✝ =
    (((TensorProduct.AlgebraTensorModule.curry ((linearize k G (X ⊗ Y)) g ∘ₗ ↑(MonoidAlgebra.tensorEquiv k)) ∘ₗ
                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
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:
ext

Goal state after:
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
a✝ : (X ⊗ Y).V
⊢ ((μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s)).coeff a✝ =
    (MonoidAlgebra.single (x, y) (r * s)).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
y : Y.V
r s : k
⊢ (μ X Y) (MonoidAlgebra.single x r ⊗ₜ[k] MonoidAlgebra.single y s) = MonoidAlgebra.single (x, y) (r * s)

Tactic:
ext; simp [← toLinearMap_apply]

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

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
⊢ (μ Z Y).comp (lTensor (linearize k G Z) (linearizeMap f)) = (linearizeMap (Z ◁ f)).comp (μ Z X)

Tactic:
ext

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
⊢ ↑(lid k (linearize k G X)) =
    ((linearizeMap (λ_ X).hom).comp (μ (𝟙_ (Action (Type w) G)) X)).comp (rTensor (linearize k G X) (ε k G))

Tactic:
ext

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

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

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
⊢ (lTensor (linearize k G Z) (linearizeMap f)).comp (δ Z X) = (δ Z Y).comp (linearizeMap (Z ◁ f))

Tactic:
ext

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

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

Goal state after:
G : Type v
inst✝¹ : Monoid G
k : Type u
inst✝ : CommSemiring k
X : Action (Type u) G
x✝ : X.V
⊢ ((↑(lid k (linearize k G X)).symm).toLinearMap ∘ₗ MonoidAlgebra.lsingle x✝) 1 =
    ((((rTensor (linearize k G X) (η k G)).comp (δ (𝟙_ (Action (Type u) G)) X)).comp
            (linearizeMap (λ_ X).inv)).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
⊢ ↑(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:
ext

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 Y).comp (δ X Y) = IntertwiningMap.id (linearize k G (X ⊗ Y))

Tactic:
ext

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 Y).comp (μ X Y) = IntertwiningMap.id ((linearize k G X).tprod (linearize k G Y))

Tactic:
ext

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
⊢ ↑(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:
ext

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
⊢ ((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:
ext

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.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:
ext

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
⊢ ↑(TensorProduct.finsuppLeft k k V W α) ∘ₗ ((σ.finsupp α).tprod ρ) g =
    ((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppLeft k k V W α)

Tactic:
ext

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
⊢ ↑(TensorProduct.finsuppRight k k V W α) ∘ₗ (σ.tprod (ρ.finsupp α)) g =
    ((σ.tprod ρ).finsupp α) g ∘ₗ ↑(TensorProduct.finsuppRight k k V W α)

Tactic:
ext

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.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 : 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) ∘ₗ
      ((leftRegular k G).tprod (trivial k G k[α])) g =
    (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)

Tactic:
ext

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

Tactic:
ext

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