∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] {X Y : CategoryTheory.Core C}
  (f : CategoryTheory.CoreHom X Y),
  { iso := { iso := f.iso.symm }.iso ≪≫ f.iso } = { iso := CategoryTheory.Iso.refl Y.of }