∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : Small.{u_3, u_1} C]
  (x : CategoryTheory.Arrow C),
  ((CategoryTheory.Shrink.equivalence C).inverse.mapArrow.obj
        ((CategoryTheory.Shrink.equivalence C).functor.mapArrow.obj x)).left =
    x.left