∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type w)} {X Y : C}
  (e : Y ≅ X) (R : F.CorepresentableBy Y),
  (CategoryTheory.Functor.CorepresentableBy.equivOfIsoObj e).symm R = R.ofIsoObj e.symm