∀ (V : Type u_2) [inst : CategoryTheory.Category.{u_1, u_2} V] {G : Type u_3} {H : Type u_4} [inst_1 : Monoid G]
  [inst_2 : Monoid H] {f f' : G →* H},
  f = f' →
    ∀ (x : Action V H) (g : G),
      CategoryTheory.CategoryStruct.comp (((Action.res V f).obj x).ρ g)
          (CategoryTheory.Iso.refl ((Action.res V f).obj x).V).hom =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Iso.refl ((Action.res V f).obj x).V).hom
          (((Action.res V f').obj x).ρ g)