awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
h :
  ∀ (a : Z.V) (a_1 : X.V),
    Eq (α := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k)
      ((((TensorProduct.AlgebraTensorModule.curry
                      (toLinearMap (comp (μ Z Y) (lTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                    Finsupp.lsingle a :
                  k →ₗ[k]
                    Finsupp.{w, u} X.V k →ₗ[k]
                      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
                (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
              1 ∘ₗ
            Finsupp.lsingle a_1 :
          (a : k) → (Z ⊗ Y).V →₀ k)
        1)
      ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (Z ◁ f)) (μ Z X))) ∘ₗ
                    Finsupp.lsingle a :
                  k →ₗ[k]
                    Finsupp.{w, u} X.V k →ₗ[k]
                      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
                (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
              1 ∘ₗ
            Finsupp.lsingle a_1 :
          (a : k) → (Z ⊗ Y).V →₀ k)
        1)
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} Z.V k) (Finsupp.{w, u} X.V k))
      (tprod (linearize k G Z) (linearize k G X))
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y)))
    (comp (μ Z Y) (lTensor (linearize k G Z) (linearizeMap f))) (comp (linearizeMap (Z ◁ f)) (μ Z X))

Tactic:
ext : 6
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
Z : Action (Type w) G
a : Z.V
a_1 : X.V
⊢ Eq (α := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k)
    ((((TensorProduct.AlgebraTensorModule.curry
                    (toLinearMap (comp (μ Z Y) (lTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                  Finsupp.lsingle a :
                k →ₗ[k]
                  Finsupp.{w, u} X.V k →ₗ[k]
                    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → (Z ⊗ Y).V →₀ k)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (Z ◁ f)) (μ Z X))) ∘ₗ
                  Finsupp.lsingle a :
                k →ₗ[k]
                  Finsupp.{w, u} X.V k →ₗ[k]
                    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Z Y).V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] (Z ⊗ Y).V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle a_1 :
        (a : k) → (Z ⊗ Y).V →₀ k)
      1)

Tactic:
simp [linearizeMap_single _]

Premises used: Representation.linearizeMap_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ Eq (α :=
    Finsupp.{w, u}
      (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V
      k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : ((X ⊗ Y) ⊗ Z).V →₀ k) → (X ⊗ Y ⊗ Z).V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u}
        (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
            (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V
        k)
    (Finsupp.single
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (fun (X : Type w) ↦ X) ((X ⊗ Y) ⊗ Z).V) → (fun (X : Type w) ↦ X) (X ⊗ Y ⊗ Z).V)
          ((x, y), z))
        1 :
      Finsupp.{w, u}
        ((fun (X : Type w) ↦ X)
          (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X
              (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)).V)
        k)

Tactic:
dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)

Premises used: id, Prod.mk, Representation.linearizeMap_single, OfNat.ofNat, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
h₁ :
  y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1
h₂ :
  z =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.2
⊢ Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)

Tactic:
convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)

Premises used: Prod.mk, Representation.linearizeMap_single, OfNat.ofNat, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
h :
  x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1
h₁ :
  y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1
h₂ :
  z =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.2
⊢ Eq (α := Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    ((linearizeMap (Iso.hom (α_ X Y Z)) : (a : (X.V × Y.V) × Z.V →₀ k) → X.V × Y.V × Z.V →₀ k)
        (Finsupp.single ((x, y), z) 1) :
      Finsupp.{w, u} (X.V × Y.V × Z.V) k)
    (Finsupp.single (x, y, z) 1 : Finsupp.{w, u} (X.V × Y.V × Z.V) k)

Tactic:
with_reducible convert! dsimp% linearizeMap_single (α_ X Y Z).hom ((x, y), z) (1 : k)

Premises used: Prod.mk, Representation.linearizeMap_single, OfNat.ofNat, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ x =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
          (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
        ((x, y), z)).1

Tactic:
with_reducible simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ y =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.1

Tactic:
with_reducible simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ z =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.2

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
z : Z.V
⊢ z =
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (Action.Hom.hom (Iso.hom (α_ X Y Z))) :
            (a : (X.V × Y.V) × Z.V) → X.V × Y.V × Z.V)
          ((x, y), z)).2.2

Tactic:
with_reducible simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
h :
  ∀ (x1 : X.V),
    Eq (α := Finsupp.{w, u} X.V k)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (toLinearMap (ρ := tprod (trivial k G k) (linearize k G X))
                      (↑(lid k (linearize k G X)) :
                        ((trivial k G k).tprod (linearize k G X)).IntertwiningMap (linearize k G X))) :
                  k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
                (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
              1 ∘ₗ
            Finsupp.lsingle x1 :
          (a : k) → X.V →₀ k)
        1)
      ((((TensorProduct.AlgebraTensorModule.curry
                    (toLinearMap
                      (comp
                        (comp (linearizeMap (Iso.hom (λ_ X)))
                          (μ ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) X))
                        (rTensor (linearize k G X) (ε k G)))) :
                  k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
                (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
              1 ∘ₗ
            Finsupp.lsingle x1 :
          (a : k) → X.V →₀ k)
        1)
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k k (Finsupp.{w, u} X.V k)) (tprod (trivial k G k) (linearize k G X))
      (linearize k G X))
    (↑(lid k (linearize k G X)) : ((trivial k G k).tprod (linearize k G X)).IntertwiningMap (linearize k G X))
    (comp (comp (linearizeMap (Iso.hom (λ_ X))) (μ ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) X))
      (rTensor (linearize k G X) (ε k G)))

Tactic:
ext x1 : 5
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x1 : X.V
⊢ Eq (α := Finsupp.{w, u} X.V k)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap (ρ := tprod (trivial k G k) (linearize k G X))
                    (↑(lid k (linearize k G X)) :
                      ((trivial k G k).tprod (linearize k G X)).IntertwiningMap (linearize k G X))) :
                k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle x1 :
        (a : k) → X.V →₀ k)
      1)
    ((((TensorProduct.AlgebraTensorModule.curry
                  (toLinearMap
                    (comp
                      (comp (linearizeMap (Iso.hom (λ_ X))) (μ ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) X))
                      (rTensor (linearize k G X) (ε k G)))) :
                k →ₗ[k] Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
              (a : k) → (X.V →₀ k) →ₗ[k] X.V →₀ k)
            1 ∘ₗ
          Finsupp.lsingle x1 :
        (a : k) → X.V →₀ k)
      1)

Tactic:
simpa [types_tensorObj_def, types_tensorUnit_def] using
    linearizeMap_single (k := k) (λ_ X).hom (PUnit.unit, x1) _ |>.symm

Premises used: CategoryTheory.types_tensorUnit_def, CategoryTheory.MonoidalCategoryStruct.leftUnitor, Prod.mk, CategoryTheory.types_tensorObj_def, Representation.linearizeMap_single, PUnit.unit, Eq.symm, CategoryTheory.Iso.hom
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
h :
  ∀ (x a : X.V),
    Eq.{u + 1} (α := k)
      (((((TensorProduct.AlgebraTensorModule.curry
                          (toLinearMap (ρ := tprod (linearize k G X) (trivial k G k))
                            (↑(rid k (linearize k G X)) :
                              ((linearize k G X).tprod (trivial k G k)).IntertwiningMap (linearize k G X))) ∘ₗ
                        Finsupp.lsingle x :
                      k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                    (a : k) → k →ₗ[k] X.V →₀ k)
                  1 :
                (a : k) → X.V →₀ k)
              1 :
            (a : X.V) → k)
          a :
        k)
      (((((TensorProduct.AlgebraTensorModule.curry
                          (toLinearMap
                            (comp
                              (comp (linearizeMap (Iso.hom (ρ_ X)))
                                (μ X ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))))
                              (lTensor (linearize k G X) (ε k G)))) ∘ₗ
                        Finsupp.lsingle x :
                      k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                    (a : k) → k →ₗ[k] X.V →₀ k)
                  1 :
                (a : k) → X.V →₀ k)
              1 :
            (a : X.V) → k)
          a :
        k)
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} X.V k) k) (tprod (linearize k G X) (trivial k G k))
      (linearize k G X))
    (↑(rid k (linearize k G X)) : ((linearize k G X).tprod (trivial k G k)).IntertwiningMap (linearize k G X))
    (comp (comp (linearizeMap (Iso.hom (ρ_ X))) (μ X ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))))
      (lTensor (linearize k G X) (ε k G)))

Tactic:
ext x
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x a : X.V
⊢ Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                        (toLinearMap (ρ := tprod (linearize k G X) (trivial k G k))
                          (↑(rid k (linearize k G X)) :
                            ((linearize k G X).tprod (trivial k G k)).IntertwiningMap (linearize k G X))) ∘ₗ
                      Finsupp.lsingle x :
                    k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                  (a : k) → k →ₗ[k] X.V →₀ k)
                1 :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry
                        (toLinearMap
                          (comp
                            (comp (linearizeMap (Iso.hom (ρ_ X)))
                              (μ X ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))))
                            (lTensor (linearize k G X) (ε k G)))) ∘ₗ
                      Finsupp.lsingle x :
                    k →ₗ[k] k →ₗ[k] Finsupp.{w, u} X.V k) :
                  (a : k) → k →ₗ[k] X.V →₀ k)
                1 :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a :
      k)

Tactic:
simp [types_tensorObj_def, types_tensorUnit_def, Action.tensorObj_V, linearizeMap,
    Action.rightUnitor_hom_hom]

Premises used: Action.tensorObj_V, CategoryTheory.types_tensorUnit_def, CategoryTheory.types_tensorObj_def, Action.rightUnitor_hom_hom, Representation.linearizeMap
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
h :
  ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
    Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
      ((((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
                (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
              (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                  (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
                g) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
        1)
      ((((tprod (linearize k G X) (linearize k G Y) :
                  (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
                g ∘ₗ
              (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
                (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
        1)
⊢ Eq (α :=
    Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k →ₗ[k]
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
        (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
          (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
        g)
    ((tprod (linearize k G X) (linearize k G Y) :
          (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
        g ∘ₗ
      (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
        (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
h :
  Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    (Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V))
                    g) :
                (a : X.V × Y.V) → X.V × Y.V)
              a).1
          1 ⊗ₜ[k]
        Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V))
                    g) :
                (a : X.V × Y.V) → X.V × Y.V)
              a).2
          1 :
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    (Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : X.V) → X.V) a.1)
          1 ⊗ₜ[k]
        Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V) a.2)
          1 :
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
⊢ Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((((↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k)) ∘ₗ
            (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y) :
                (a : G) → ((X ⊗ Y).V →₀ k) →ₗ[k] (X ⊗ Y).V →₀ k)
              g) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)
    ((((tprod (linearize k G X) (linearize k G Y) :
                (a : G) → TensorProduct k (X.V →₀ k) (Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))
              g ∘ₗ
            (↑(LinearEquiv.symm (finsuppTensorFinsupp' k X.V Y.V)) :
              (X.V × Y.V →₀ k) →ₗ[k] TensorProduct k (X.V →₀ k) (Y.V →₀ k))) ∘ₗ
          Finsupp.lsingle a :
        (a : k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k))
      1)

Tactic:
simp [types_tensorObj_def, linearize_single _,
      finsuppTensorFinsupp'_symm_single_eq_single_one_tmul k]

Premises used: Representation.linearize_single, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, CategoryTheory.types_tensorObj_def
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k_1 : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k_1
inst_2 : AddCommGroup V
inst_3 : Module k_1 V
inst_4 : AddCommGroup W
inst_5 : Module k_1 W
σ_1 : Representation k_1 G V
ρ_1 : Representation k_1 G W
X Y Z : Action (Type w) G
k : Type u
inst_6 : CommSemiring k
inst_7 : Module k V
inst_8 : Module k W
σ : Representation k G V
ρ : Representation k G W
g : G
a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    (Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V))
                    g) :
                (a : X.V × Y.V) → X.V × Y.V)
              a).1
          1 ⊗ₜ[k]
        Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X.V × Y.V))
                    g) :
                (a : X.V × Y.V) → X.V × Y.V)
              a).2
          1 :
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    (Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : X.V) → X.V) a.1)
          1 ⊗ₜ[k]
        Finsupp.single
          ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V) a.2)
          1 :
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
xy : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq (α := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    ((δ X Y : (a : (X ⊗ Y).V →₀ k) → TensorProduct k (X.V →₀ k) (Y.V →₀ k)) (Finsupp.single xy 1) :
      TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))
    (Finsupp.single xy.1 1 ⊗ₜ[k] Finsupp.single xy.2 1 : TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Y.V k))

Tactic:
simp [δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul k]

Premises used: Representation.LinearizeMonoidal.δ, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y Z : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
f : X ⟶ Y
h :
  ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z).V),
    Eq (α := TensorProduct k (Finsupp.{w, u} Y.V k) (Finsupp.{w, u} Z.V k))
      ((toLinearMap (comp (rTensor (linearize k G Z) (linearizeMap f)) (δ X Z)) ∘ₗ Finsupp.lsingle a :
          (a : k) → TensorProduct k (Y.V →₀ k) (Z.V →₀ k))
        1)
      ((toLinearMap (comp (δ Y Z) (linearizeMap (f ▷ Z))) ∘ₗ Finsupp.lsingle a :
          (a : k) → TensorProduct k (Y.V →₀ k) (Z.V →₀ k))
        1)
⊢ Eq (α :=
    IntertwiningMap (V := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z).V k)
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Z))
      (tprod (linearize k G Y) (linearize k G Z)))
    (comp (rTensor (linearize k G Z) (linearizeMap f)) (δ X Z)) (comp (δ Y Z) (linearizeMap (f ▷ Z)))

Tactic:
ext