∀ {G : Type u_1} [inst : Group G] (N : Subgroup G) [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] (g h : G),
  (CategoryTheory.ConcreteCategory.hom ((Action.FintypeCat.toEndHom N) g).hom) ⟦h⟧ = ⟦h * g⁻¹⟧