-- Module: Mathlib.RepresentationTheory.Tannaka
Goal:
k G : Type u
inst : CommRing k
inst_1 : Group G
inst_2 : Finite G
g : G
u :
  (↑(ObjectProperty.FullSubcategory.obj (P := isFG k)
        (Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))) :
    Type u)
x x_1 :
  TensorProduct k (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
    (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u)
hx :
  Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                    (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                  g)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        x :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
hy :
  Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                    (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                  g)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        x_1 :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        x_1 :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
⊢ Eq (α := (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep))
                ((Action.ρ (tensorObj (𝒞 := Action.instCategory) rightFDRep rightFDRep) :
                    (a : G) → End (rightFDRep ⊗ rightFDRep).V)
                  g)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k)))))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        (x + x_1) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))
    ((Hom.hom
            (InducedCategory.Hom.hom
              (CategoryStruct.comp (Y := Action.V (G := G) rightFDRep)
                (InducedCategory.homMk (↟(LinearMap.mul' k (G → k))))
                ((Action.ρ rightFDRep : (a : G) → End rightFDRep.V) g))) :
          (a : (↑(rightFDRep ⊗ rightFDRep).V.obj : Type u)) → (↑rightFDRep.V.obj : Type u))
        (x + x_1) :
      (↑(ObjectProperty.FullSubcategory.obj (P := isFG k) (Action.V (G := G) rightFDRep)) : Type u))

Tactic:
simp only [map_add, hx, hy]

Premises used: map_add