awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : tensorObj (𝒞 := instCategory) A B ⟶ C
⊢ Representation.IntertwiningMap.toLinearMap
      (Hom.hom ((linearHomEquivComm A B C : (a : A ⊗ B ⟶ C) → A ⟶ (ihom B).obj C) f)) =
    TensorProduct.curry (Hom.hom f).toLinearMap

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, TensorProduct.curry, LinearMap.compr₂ₛₗ, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : B ⟶ Functor.obj (ihom A) C
simp :
  Eq.{u + 1} (α := TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
    (Representation.IntertwiningMap.toLinearMap.{u, v, u, u} (G := G) (ρ := A.ρ.tprod B.ρ) (σ := C.ρ)
        (Hom.hom (((A.tensorHomEquiv B C).symm : (a : B ⟶ (ihom A).obj C) → A ⊗ B ⟶ C) f)) :
      TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
          (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
            TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
        (Hom.hom f).flip :
      TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
⊢ Eq.{u + 1} (α := (↑(tensorObj (𝒞 := instCategory) A B) : Type u) →ₗ[k] (↑C : Type u))
    (Representation.IntertwiningMap.toLinearMap
      (Hom.hom (((linearHomEquiv A B C).symm : (a : B ⟶ (ihom A).obj C) → A ⊗ B ⟶ C) f)))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
        (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
          TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
      (Hom.hom f).flip)

Tactic:
simp [linearHomEquiv]

Premises used: Rep.MonoidalClosed.linearHomEquiv
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : B ⟶ Functor.obj (ihom A) C
⊢ Eq.{u + 1} (α := TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
    (Representation.IntertwiningMap.toLinearMap.{u, v, u, u} (G := G) (ρ := A.ρ.tprod B.ρ) (σ := C.ρ)
        (Hom.hom (((A.tensorHomEquiv B C).symm : (a : B ⟶ (ihom A).obj C) → A ⊗ B ⟶ C) f)) :
      TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
          (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
            TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
        (Hom.hom f).flip :
      TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))

Tactic:
rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : CommRing k
G : Type v
inst_1 : Group G
A B C : Rep k G
f : A ⟶ Functor.obj (ihom B) C
⊢ Eq.{u + 1} (α := (↑(tensorObj (𝒞 := instCategory) A B) : Type u) →ₗ[k] (↑C : Type u))
    (Representation.IntertwiningMap.toLinearMap
      (Hom.hom (((linearHomEquivComm A B C).symm : (a : A ⟶ (ihom B).obj C) → A ⊗ B ⟶ C) f)))
    ((TensorProduct.uncurry (RingHom.id k) (↑A : Type u) (↑B : Type u) (↑C : Type u) :
        (a : (↑A : Type u) →ₗ[k] (↑B : Type u) →ₗ[k] (↑C : Type u)) →
          TensorProduct k (↑A : Type u) (↑B : Type u) →ₗ[k] (↑C : Type u))
      (Hom.hom f).toLinearMap)

Tactic:
TensorProduct.ext' fun _ _ => rfl

Premises used: Quotient, TensorProduct, AddCon.Quotient, TensorProduct.ext', rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
k : Type u
inst_2 : Semiring k
G : Type v
inst_3 : Group G
inst_4 : Fintype G
A : Rep.{w, u, v} k G
g : G
h :
  ∀ (x : (↑A : Type w)),
    Eq (α := (↑A : Type w))
      ((A.ρ.norm ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (a : (↑A : Type w)) → (↑A : Type w)) x :
        (↑A : Type w))
      (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ A.ρ.norm : (a : (↑A : Type w)) → (↑A : Type w)) x :
        (↑A : Type w))
⊢ A.ρ.norm ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g =
    (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ A.ρ.norm

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k_1 : Type u
G_1 : Type v
inst : CommRing k_1
inst_1 : Monoid G_1
k : Type u
inst_2 : Semiring k
G : Type v
inst_3 : Group G
inst_4 : Fintype G
A : Rep.{w, u, v} k G
g : G
x : (↑A : Type w)
⊢ Eq (α := (↑A : Type w))
    ((A.ρ.norm ∘ₗ (A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g : (a : (↑A : Type w)) → (↑A : Type w)) x :
      (↑A : Type w))
    (((A.ρ : (a : G) → (↑A : Type w) →ₗ[k] (↑A : Type w)) g ∘ₗ A.ρ.norm : (a : (↑A : Type w)) → (↑A : Type w)) x :
      (↑A : Type w))

Tactic:
simp
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
A : Rep.{w, u, v} k G
x : (↑A : Type w)
⊢ Eq (α := (↑A : Type w)) ((Hom.hom A.norm : (a : (↑A : Type w)) → (↑A : Type w)) x : (↑A : Type w))
    ((A.ρ.norm : (a : (↑A : Type w)) → (↑A : Type w)) x : (↑A : Type w))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
hf :
  ∀ (x : (↑A : Type u_1)),
    Eq (α := (↑B : Type u_1))
      (((Hom.hom (f ≫ B.norm)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
      (((Hom.hom (A.norm ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
⊢ f ≫ B.norm = A.norm ≫ f

Tactic:
ext
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
inst : Semiring k
G : Type v
inst_1 : Group G
inst_2 : Fintype G
A B : Rep.{u_1, u, v} k G
f : A ⟶ B
x : (↑A : Type u_1)
⊢ Eq (α := (↑B : Type u_1))
    (((Hom.hom (f ≫ B.norm)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))
    (((Hom.hom (A.norm ≫ f)).toLinearMap : (a : (↑A : Type u_1)) → (↑B : Type u_1)) x : (↑B : Type u_1))

Tactic:
simp [Representation.norm, hom_comm_apply]

Premises used: Rep.hom_comm_apply, Representation.norm
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
α : Type u'
A : Rep.{u_1, u, v} k G
⊢ (↑(finsupp α A) : Type (max u' u_1)) = Finsupp.{u', u_1} α (↑A : Type u_1)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
α : Type u'
A : Rep.{u_1, u, v} k G
f : sorry ⟶ A
g : sorry ⟶ A
h :
  ∀ (i : α),
    Eq (α := (↑A : Type u_1)) ((Hom.hom f : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
      ((Hom.hom g : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
⊢ f = g

Tactic:
(freeLiftLEquiv k G α A).injective (funext_iff.2 h)

Premises used: Iff.mpr, Unit.unit, funext_iff, sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, Bool.true, Function.const, Lean.Name, Rep.freeLiftLEquiv, LinearEquiv.injective, OfNat.ofNat
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
α : Type u'
A : Rep.{u_1, u, v} k G
f : sorry ⟶ A
g : sorry ⟶ A
h :
  ∀ (i : α),
    Eq (α := (↑A : Type u_1)) ((Hom.hom f : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
      ((Hom.hom g : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
⊢ f = g

Tactic:
exact (freeLiftLEquiv k G α A).injective (funext_iff.2 h)

Premises used: Iff.mpr, funext_iff, Rep.freeLiftLEquiv, LinearEquiv.injective
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
α : Type u'
A : Rep.{u_1, u, v} k G
f : sorry ⟶ A
g : sorry ⟶ A
h :
  ∀ (i : α),
    Eq (α := (↑A : Type u_1)) ((Hom.hom f : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
      ((Hom.hom g : (a : (↑sorry : Type u_1)) → (↑A : Type u_1)) sorry : (↑A : Type u_1))
⊢ f = g

Tactic:
classical exact (freeLiftLEquiv k G α A).injective (funext_iff.2 h)

Premises used: Iff.mpr, funext_iff, Rep.freeLiftLEquiv, LinearEquiv.injective
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
f : X ⟶ Y
hf :
  Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
        Type u))
      (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
    (Hom.hom (Functor.obj (linearization k G) Z ◁ CategoryTheory.Functor.map (linearization k G) f ≫ ofHom (μ Z Y)) :
      Representation.IntertwiningMap (V :=
        (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
          Type u))
        (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
        (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
        (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
    (Hom.hom (ofHom (μ Z X) ≫ CategoryTheory.Functor.map (linearization k G) (Z ◁ f)) :
      Representation.IntertwiningMap (V :=
        (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
          Type u))
        (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
        (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
        (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G)
      (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
      (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))
    (Functor.obj (linearization k G) Z ◁ CategoryTheory.Functor.map (linearization k G) f ≫ ofHom (μ Z Y) :
      Quiver.Hom (V := Rep k G)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
        (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))
    (ofHom (μ Z X) ≫ CategoryTheory.Functor.map (linearization k G) (Z ◁ f) :
      Quiver.Hom (V := Rep k G)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X))
        (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)))

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
f : X ⟶ Y
⊢ Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
        Type u))
      (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
    (Hom.hom (Functor.obj (linearization k G) Z ◁ CategoryTheory.Functor.map (linearization k G) f ≫ ofHom (μ Z Y)) :
      Representation.IntertwiningMap (V :=
        (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
          Type u))
        (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
        (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
        (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))
    (Hom.hom (ofHom (μ Z X) ≫ CategoryTheory.Functor.map (linearization k G) (Z ◁ f)) :
      Representation.IntertwiningMap (V :=
        (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)) :
          Type u))
        (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y)) : Type u))
        (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) Z) (Functor.obj (linearization k G) X)))
        (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Z Y))))

Tactic:
simp [μ_comp_lTensor _]

Premises used: Representation.LinearizeMonoidal.μ_comp_lTensor
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
hf :
  Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory)
            (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
            (Functor.obj (linearization k G) Z)) :
        Type u))
      (W :=
      (↑(Functor.obj (linearization k G)
            (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z))) :
        Type u))
      (ρ
        (tensorObj (𝒞 := instCategory)
          (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
          (Functor.obj (linearization k G) Z)))
      (ρ
        (Functor.obj (linearization k G)
          (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z)))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
          (Functor.obj (linearization k G) Z))
        (ofHom (μ X Y) ▷ Functor.obj (linearization k G) Z)
        (ofHom (μ (tensorObj (𝒞 := Action.instCategory) X Y) Z) ≫
          CategoryTheory.Functor.map (linearization k G) (Iso.hom (α_ X Y Z)))))
    (Hom.hom
      (Iso.hom
          (α_ (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)
            (Functor.obj (linearization k G) Z)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X)
            (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Y Z)))
          (Functor.obj (linearization k G) X ◁ ofHom (μ Y Z)) (ofHom (μ X (tensorObj (𝒞 := Action.instCategory) Y Z)))))
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G)
      (tensorObj (𝒞 := instCategory)
        (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
        (Functor.obj (linearization k G) Z))
      (Functor.obj (linearization k G)
        (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z))))
    (CategoryStruct.comp (Y :=
      tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
        (Functor.obj (linearization k G) Z))
      (ofHom (μ X Y) ▷ Functor.obj (linearization k G) Z)
      (ofHom (μ (tensorObj (𝒞 := Action.instCategory) X Y) Z) ≫
        CategoryTheory.Functor.map (linearization k G) (Iso.hom (α_ X Y Z))))
    (Iso.hom
        (α_ (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)
          (Functor.obj (linearization k G) Z)) ≫
      CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X)
          (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Y Z)))
        (Functor.obj (linearization k G) X ◁ ofHom (μ Y Z)) (ofHom (μ X (tensorObj (𝒞 := Action.instCategory) Y Z))))

Tactic:
ext1
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y Z : Action (Type u) G
⊢ Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory)
            (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
            (Functor.obj (linearization k G) Z)) :
        Type u))
      (W :=
      (↑(Functor.obj (linearization k G)
            (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z))) :
        Type u))
      (ρ
        (tensorObj (𝒞 := instCategory)
          (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
          (Functor.obj (linearization k G) Z)))
      (ρ
        (Functor.obj (linearization k G)
          (tensorObj (𝒞 := Action.instCategory) X (tensorObj (𝒞 := Action.instCategory) Y Z)))))
    (Hom.hom
      (CategoryStruct.comp (Y :=
        tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
          (Functor.obj (linearization k G) Z))
        (ofHom (μ X Y) ▷ Functor.obj (linearization k G) Z)
        (ofHom (μ (tensorObj (𝒞 := Action.instCategory) X Y) Z) ≫
          CategoryTheory.Functor.map (linearization k G) (Iso.hom (α_ X Y Z)))))
    (Hom.hom
      (Iso.hom
          (α_ (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)
            (Functor.obj (linearization k G) Z)) ≫
        CategoryStruct.comp (Y :=
          tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X)
            (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) Y Z)))
          (Functor.obj (linearization k G) X ◁ ofHom (μ Y Z)) (ofHom (μ X (tensorObj (𝒞 := Action.instCategory) Y Z)))))

Tactic:
simp [μ_comp_assoc _]

Premises used: Representation.LinearizeMonoidal.μ_comp_assoc
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Action (Type u) G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G)
      (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))
      (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y)))
    (Functor.LaxMonoidal.μ (linearization k G) X Y) (ofHom (Representation.LinearizeMonoidal.μ X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Action (Type u) G
⊢ Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)) :
        Type u))
      (W := (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y)) : Type u))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))))
    (Hom.hom (Functor.LaxMonoidal.μ (linearization k G) X Y)) (Representation.LinearizeMonoidal.μ X Y)

Tactic:
rfl

Premises used: Representation.LinearizeMonoidal.μ, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) ((𝟙_ (Rep k G)) (𝒞 := instCategory))
      (Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
    (Functor.LaxMonoidal.ε (linearization k G)) (ofHom (Representation.LinearizeMonoidal.ε k G))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α :=
    Representation.IntertwiningMap (V := (↑((𝟙_ (Rep k G)) (𝒞 := instCategory)) : Type u)) (W :=
      (↑(Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))) : Type u))
      (ρ ((𝟙_ (Rep k G)) (𝒞 := instCategory)))
      (ρ (Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))))
    (Hom.hom (Functor.LaxMonoidal.ε (linearization k G))) (Representation.LinearizeMonoidal.ε k G)

Tactic:
rfl

Premises used: Representation.LinearizeMonoidal.ε, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Action (Type u) G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y))
      (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)))
    (Functor.OplaxMonoidal.δ (linearization k G) X Y) (ofHom (Representation.LinearizeMonoidal.δ X Y))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
X Y : Action (Type u) G
⊢ Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y)) : Type u)) (W :=
      (↑(tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y)) :
        Type u))
      (ρ (Functor.obj (linearization k G) (tensorObj (𝒞 := Action.instCategory) X Y)))
      (ρ (tensorObj (𝒞 := instCategory) (Functor.obj (linearization k G) X) (Functor.obj (linearization k G) Y))))
    (Hom.hom (Functor.OplaxMonoidal.δ (linearization k G) X Y)) (Representation.LinearizeMonoidal.δ X Y)

Tactic:
rfl

Premises used: Representation.LinearizeMonoidal.δ, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α :=
    Quiver.Hom (V := Rep k G) (Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory)))
      ((𝟙_ (Rep k G)) (𝒞 := instCategory)))
    (Functor.OplaxMonoidal.η (linearization k G)) (ofHom (Representation.LinearizeMonoidal.η k G))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
⊢ Eq (α :=
    Representation.IntertwiningMap (V :=
      (↑(Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))) : Type u)) (W :=
      (↑((𝟙_ (Rep k G)) (𝒞 := instCategory)) : Type u))
      (ρ (Functor.obj (linearization k G) ((𝟙_ (Action (Type u) G)) (𝒞 := Action.instCategory))))
      (ρ ((𝟙_ (Rep k G)) (𝒞 := instCategory))))
    (Hom.hom (Functor.OplaxMonoidal.η (linearization k G))) (Representation.LinearizeMonoidal.η k G)

Tactic:
rfl

Premises used: Representation.LinearizeMonoidal.η, rfl
-- Module: Mathlib.RepresentationTheory.Rep.Basic
Goal:
k : Type u
G : Type v
inst : CommRing k
inst_1 : Monoid G
A : Rep k G
x : (↑A : Type (max u v))
g : G
⊢ Eq (α := (↑A : Type (max u v)))
    ((Hom.hom ((A.leftRegularHomEquiv.symm : (a : (↑A : Type (max u v))) → leftRegular k G ⟶ A) x) :
          (a : (↑(leftRegular k G) : Type (max u v))) → (↑A : Type (max u v)))
        (Finsupp.single g 1) :
      (↑A : Type (max u v)))
    ((((A.ρ : (a : G) → (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) g :
            (↑A : Type (max u v)) →ₗ[k] (↑A : Type (max u v))) :
          (a : (↑A : Type (max u v))) → (↑A : Type (max u v)))
        x :
      (↑A : Type (max u v)))

Tactic:
simp [homEquiv]

Premises used: Rep.homEquiv