awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
x x_1 : G
a a_1 : X.V
⊢ Eq.{u + 1} (α := k)
    (((Finsupp.lmapDomain k k
                  (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) (x * x_1))) :
                    (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)
    (((HMul.hMul (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k)
                  (Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x)) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V))
                  (Finsupp.lmapDomain k k
                    (⇑(@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) x_1)) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V)) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → X.V →₀ k)
            1 :
          (a : X.V) → k)
        a_1 :
      k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X : Action (Type w) G
g : G
x : X.V
⊢ Eq (α := Finsupp.{w, u} X.V k)
    ((((linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g : Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} X.V k) :
          (a : X.V →₀ k) → X.V →₀ k)
        (Finsupp.single x 1) :
      Finsupp.{w, u} X.V k)
    (Finsupp.single
        ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) :
            (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V)
          x)
        1 :
      Finsupp.{w, u} ((fun (X : Type w) ↦ X) X.V) k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
h :
  ∀ (x : X.V) (y : Y.V),
    Eq.{u + 1} (α := k)
      ((((Finsupp.lmapDomain k k
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V) ∘ₗ
                    (linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g) ∘ₗ
                  Finsupp.lsingle x :
                (a : k) → Y.V →₀ k)
              1 :
            (a : Y.V) → k)
          y :
        k)
      (((((linearize k G Y : (a : G) → (Y.V →₀ k) →ₗ[k] Y.V →₀ k) g ∘ₗ
                    Finsupp.lmapDomain k k
                      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V)) ∘ₗ
                  Finsupp.lsingle x :
                (a : k) → Y.V →₀ k)
              1 :
            (a : Y.V) → k)
          y :
        k)
⊢ Eq (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} Y.V k)
    (Finsupp.lmapDomain k k
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V) ∘ₗ
      (linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g)
    ((linearize k G Y : (a : G) → (Y.V →₀ k) →ₗ[k] Y.V →₀ k) g ∘ₗ
      Finsupp.lmapDomain k k
        (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
          (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V))

Tactic:
ext x y
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
f : X ⟶ Y
g : G
x : X.V
y : Y.V
⊢ Eq.{u + 1} (α := k)
    ((((Finsupp.lmapDomain k k
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V) ∘ₗ
                  (linearize k G X : (a : G) → (X.V →₀ k) →ₗ[k] X.V →₀ k) g) ∘ₗ
                Finsupp.lsingle x :
              (a : k) → Y.V →₀ k)
            1 :
          (a : Y.V) → k)
        y :
      k)
    (((((linearize k G Y : (a : G) → (Y.V →₀ k) →ₗ[k] Y.V →₀ k) g ∘ₗ
                  Finsupp.lmapDomain k k
                    (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
                      (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V)) ∘ₗ
                Finsupp.lsingle x :
              (a : k) → Y.V →₀ k)
            1 :
          (a : Y.V) → k)
        y :
      k)

Tactic:
simp [(congr($(f.comm g) x) : f.hom (X.ρ g x) = Y.ρ g (f.hom x))]

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, DFunLike.coe, Action.Hom.comm
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X Y : Action (Type w) G
f : X ⟶ Y
x : X.V
r : k
⊢ Eq (α := Finsupp.{w, u} Y.V k)
    ((linearizeMap f : (a : X.V →₀ k) → Y.V →₀ k) (Finsupp.single x r) : Finsupp.{w, u} Y.V k)
    (Finsupp.single
        ((ConcreteCategory.hom (FC := TypeCat.Fun) f.hom :
            (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V)
          x)
        r :
      Finsupp.{w, u} ((fun (X : Type w) ↦ X) Y.V) k)

Tactic:
simp [linearizeMap]

Premises used: Representation.linearizeMap
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
X Y : Action (Type w) G
f : X ⟶ Y
⊢ Eq (α := Finsupp.{w, u} X.V k →ₗ[k] Finsupp.{w, u} Y.V k) (toLinearMap (linearizeMap f))
    (Finsupp.lmapDomain k k
      (⇑(ConcreteCategory.hom (FC := TypeCat.Fun) f.hom) :
        (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) Y.V))

Tactic:
rfl

Premises used: Finsupp.lmapDomain, rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
g : G
xy : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq (α := (fun (X : Type w) ↦ X) (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V)
    ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
            (((MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).ρ : (a : G) → End (X ⊗ Y).V) g) :
          (a : (fun (X : Type w) ↦ X) (X ⊗ Y).V) → (fun (X : Type w) ↦ X) (X ⊗ Y).V)
        xy :
      (fun (X : Type w) ↦ X) (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V)
    (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) :
            (a : (fun (X : Type w) ↦ X) X.V) → (fun (X : Type w) ↦ X) X.V)
          xy.1,
        (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) :
            (a : (fun (X : Type w) ↦ X) Y.V) → (fun (X : Type w) ↦ X) Y.V)
          xy.2) :
      (fun (X : Type w) ↦ X) X.V × (fun (X : Type w) ↦ X) Y.V)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
h :
  Eq (α := Finsupp.{w, u} (Action.V.{w, w + 1, v} (G := G) ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))) k)
    (((↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) ∘ₗ
          ((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g :
        (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
      1)
    (((linearize k G ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) :
              (a : G) → ((𝟙_ (Action (Type w) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type w) G)).V →₀ k)
            g ∘ₗ
          (↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) :
        (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
      1)
⊢ Eq (α :=
    k →ₗ[k] Finsupp.{w, u} (Action.V.{w, w + 1, v} (G := G) ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))) k)
    ((↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) ∘ₗ
      ((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g)
    ((linearize k G ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) :
          (a : G) → ((𝟙_ (Action (Type w) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type w) G)).V →₀ k)
        g ∘ₗ
      (↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k))

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
⊢ Eq (α := Finsupp.{w, u} (Action.V.{w, w + 1, v} (G := G) ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory))) k)
    (((↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) ∘ₗ
          ((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g :
        (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
      1)
    (((linearize k G ((𝟙_ (Action (Type w) G)) (𝒞 := Action.instCategory)) :
              (a : G) → ((𝟙_ (Action (Type w) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type w) G)).V →₀ k)
            g ∘ₗ
          (↑(LinearEquiv.symm (Finsupp.uniqueLinearEquiv k k PUnit.unit)) : k →ₗ[k] PUnit.{w + 1} →₀ k) :
        (a : k) → (𝟙_ (Action (Type w) G)).V →₀ k)
      1)

Tactic:
simp [linearize_single _]

Premises used: Representation.linearize_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
⊢ Eq (α :=
    Finsupp.{u_1, u} (Action.V.{u_1, u_1 + 1, v} (G := G) ((𝟙_ (Action (Type u_1) G)) (𝒞 := Action.instCategory))) k)
    ((ε k G : (a : k) → (𝟙_ (Action (Type u_1) G)).V →₀ k) 1) (Finsupp.single PUnit.unit 1)

Tactic:
simp [← toLinearMap_apply, types_tensorUnit_def]

Premises used: CategoryTheory.types_tensorUnit_def, Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
h :
  ∀ (a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))),
    Eq (α := k)
      ((((↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k) ∘ₗ
                ((linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) :
                      Representation k G
                        (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)) :
                    (a : G) → ((𝟙_ (Action (Type u) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type u) G)).V →₀ k)
                  g) ∘ₗ
              Finsupp.lsingle a :
            (a : k) → k)
          1 :
        k)
      (((((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
                (↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k)) ∘ₗ
              Finsupp.lsingle a :
            (a : k) → k)
          1 :
        k)
⊢ Eq (α := (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k) →ₗ[k] k)
    ((↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k) ∘ₗ
      ((linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) :
            Representation k G
              (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)) :
          (a : G) → ((𝟙_ (Action (Type u) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type u) G)).V →₀ k)
        g)
    (((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
      (↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
V : Type u'
W : Type v'
inst : Monoid G
inst_1 : Semiring k
inst_2 : AddCommGroup V
inst_3 : Module k V
inst_4 : AddCommGroup W
inst_5 : Module k W
σ : Representation k G V
ρ : Representation k G W
X Y Z : Action (Type w) G
g : G
a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))
⊢ Eq (α := k)
    ((((↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k) ∘ₗ
              ((linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) :
                    Representation k G
                      (Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)) :
                  (a : G) → ((𝟙_ (Action (Type u) G)).V →₀ k) →ₗ[k] (𝟙_ (Action (Type u) G)).V →₀ k)
                g) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)
    (((((trivial k G k : Representation k G k) : (a : G) → k →ₗ[k] k) g ∘ₗ
              (↑(Finsupp.uniqueLinearEquiv k k PUnit.unit) : (PUnit.{u + 1} →₀ k) →ₗ[k] k)) ∘ₗ
            Finsupp.lsingle a :
          (a : k) → k)
        1 :
      k)

Tactic:
simp [linearize_single _]

Premises used: Representation.linearize_single
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
h :
  ∀ (a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
    (a_1 : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))),
    Eq (α := k)
      (((toLinearMap (comp (ε k G) (η k G)) ∘ₗ Finsupp.lsingle a : (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k) 1 :
            (a : (𝟙_ (Action (Type u) G)).V) → k)
          a_1 :
        k)
      (((toLinearMap (ρ := linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
                    (IntertwiningMap.id (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))) ∘ₗ
                  Finsupp.lsingle a :
                (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k)
              1 :
            (a : (𝟙_ (Action (Type u) G)).V) → k)
          a_1 :
        k)
⊢ Eq (α :=
    IntertwiningMap (V := Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)
      (W := Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)) →₀ k)
      (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
      (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
    (comp (ε k G) (η k G)) (IntertwiningMap.id (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
a : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))
a_1 : Action.V.{u, u + 1, v} (G := G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))
⊢ Eq (α := k)
    (((toLinearMap (comp (ε k G) (η k G)) ∘ₗ Finsupp.lsingle a : (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k) 1 :
          (a : (𝟙_ (Action (Type u) G)).V) → k)
        a_1 :
      k)
    (((toLinearMap (ρ := linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
                  (IntertwiningMap.id (linearize k G ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))) ∘ₗ
                Finsupp.lsingle a :
              (a : k) → (𝟙_ (Action (Type u) G)).V →₀ k)
            1 :
          (a : (𝟙_ (Action (Type u) G)).V) → k)
        a_1 :
      k)

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
h :
  Eq (α := k) ((toLinearMap (comp (η k G) (ε k G)) : (a : k) → k) 1 : k)
    ((toLinearMap (ρ := trivial k G k) (IntertwiningMap.id (trivial k G k)) : (a : k) → k) 1 : k)
⊢ Eq (α := IntertwiningMap (trivial k G k) (trivial k G k)) (comp (η k G) (ε k G)) (IntertwiningMap.id (trivial k G k))

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
k : Type u
G : Type v
inst : Monoid G
inst_1 : Semiring k
⊢ Eq (α := k) ((toLinearMap (comp (η k G) (ε k G)) : (a : k) → k) 1 : k)
    ((toLinearMap (ρ := trivial k G k) (IntertwiningMap.id (trivial k G k)) : (a : k) → k) 1 : k)

Tactic:
simp
-- 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 : X.V
a_1 : Y.V
a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq.{u + 1} (α := k)
    (((Finsupp.single
              ((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((X.ρ : (a : G) → End X.V) g) : (a : X.V) → X.V) a,
                (@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _ ((Y.ρ : (a : G) → End Y.V) g) : (a : Y.V) → Y.V)
                  a_1)
              1 :
            Finsupp.{w, u} (X.V × Y.V) k) :
          (a : X.V × Y.V) → k)
        a_2 :
      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, a_1))
              1 :
            Finsupp.{w, u} (X.V × Y.V) k) :
          (a : X.V × Y.V) → k)
        a_2 :
      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
x : X.V
y : Y.V
r s : k
h :
  ∀ (a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V),
    Eq.{u + 1} (α := k)
      ((((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k)
                (Finsupp.single x r ⊗ₜ[k] Finsupp.single y s) :
              Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
            (a : (X ⊗ Y).V) → k)
          a :
        k)
      ((Finsupp.single (x, y) (r * s) : (a : (X ⊗ Y).V) → k) a : k)
⊢ Eq (α := Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    ((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k)
        (Finsupp.single x r ⊗ₜ[k] Finsupp.single y s) :
      Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k)
    (Finsupp.single (x, y) (r * s) : Finsupp.{w, u} (X.V × Y.V) k)

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
x : X.V
y : Y.V
r s : k
a : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ Eq.{u + 1} (α := k)
    ((((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k)
              (Finsupp.single x r ⊗ₜ[k] Finsupp.single y s) :
            Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
          (a : (X ⊗ Y).V) → k)
        a :
      k)
    ((Finsupp.single (x, y) (r * s) : (a : (X ⊗ Y).V) → k) a : k)

Tactic:
simp [← toLinearMap_apply]

Premises used: Representation.IntertwiningMap.toLinearMap_apply
-- Module: Mathlib.RepresentationTheory.Action
Goal:
G : Type v
inst : Monoid G
X Y : Action (Type w) G
k : Type u
inst_1 : CommSemiring k
l1 : Finsupp.{w, u} X.V k
l2 : Finsupp.{w, u} Y.V k
xy : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V
⊢ (((μ X Y : (a : TensorProduct k (X.V →₀ k) (Y.V →₀ k)) → (X ⊗ Y).V →₀ k) (l1 ⊗ₜ[k] l2) :
          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) X Y).V k) :
        (a : (X ⊗ Y).V) → k)
      xy =
    HMul.hMul (α := k) (β := k) ((l1 : (a : X.V) → k) xy.1 : k) ((l2 : (a : Y.V) → k) xy.2 : k)

Tactic:
simp [← toLinearMap_apply, types_tensorObj_def, finsuppTensorFinsupp'_apply_apply _]

Premises used: finsuppTensorFinsupp'_apply_apply, Representation.IntertwiningMap.toLinearMap_apply, CategoryTheory.types_tensorObj_def
-- 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 : X.V) (a_1 : Z.V) (a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V),
    Eq.{u + 1} (α := k)
      (((((TensorProduct.AlgebraTensorModule.curry
                            (toLinearMap (comp (μ Y Z) (rTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                          Finsupp.lsingle a :
                        k →ₗ[k]
                          Finsupp.{w, u} Z.V k →ₗ[k]
                            Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                      (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                    1 ∘ₗ
                  Finsupp.lsingle a_1 :
                (a : k) → (Y ⊗ Z).V →₀ k)
              1 :
            (a : (Y ⊗ Z).V) → k)
          a_2 :
        k)
      (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (f ▷ Z)) (μ X Z))) ∘ₗ
                          Finsupp.lsingle a :
                        k →ₗ[k]
                          Finsupp.{w, u} Z.V k →ₗ[k]
                            Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                      (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                    1 ∘ₗ
                  Finsupp.lsingle a_1 :
                (a : k) → (Y ⊗ Z).V →₀ k)
              1 :
            (a : (Y ⊗ Z).V) → k)
          a_2 :
        k)
⊢ Eq (α :=
    IntertwiningMap (V := TensorProduct k (Finsupp.{w, u} X.V k) (Finsupp.{w, u} Z.V k))
      (tprod (linearize k G X) (linearize k G Z))
      (linearize k G (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z)))
    (comp (μ Y Z) (rTensor (linearize k G Z) (linearizeMap f))) (comp (linearizeMap (f ▷ Z)) (μ X Z))

Tactic:
ext
-- 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 : X.V
a_1 : Z.V
a_2 : (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V
⊢ Eq.{u + 1} (α := k)
    (((((TensorProduct.AlgebraTensorModule.curry
                          (toLinearMap (comp (μ Y Z) (rTensor (linearize k G Z) (linearizeMap f)))) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Z.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                    (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (Y ⊗ Z).V →₀ k)
            1 :
          (a : (Y ⊗ Z).V) → k)
        a_2 :
      k)
    (((((TensorProduct.AlgebraTensorModule.curry (toLinearMap (comp (linearizeMap (f ▷ Z)) (μ X Z))) ∘ₗ
                        Finsupp.lsingle a :
                      k →ₗ[k]
                        Finsupp.{w, u} Z.V k →ₗ[k]
                          Finsupp.{w, u} (MonoidalCategoryStruct.tensorObj (𝒞 := Action.instCategory) Y Z).V k) :
                    (a : k) → (Z.V →₀ k) →ₗ[k] (Y ⊗ Z).V →₀ k)
                  1 ∘ₗ
                Finsupp.lsingle a_1 :
              (a : k) → (Y ⊗ Z).V →₀ k)
            1 :
          (a : (Y ⊗ Z).V) → k)
        a_2 :
      k)

Tactic:
simp [linearizeMap_single _]

Premises used: Representation.linearizeMap_single