∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {f : CategoryTheory.Functor C D} (hf : f.FullyFaithful) (X : C) (f_1 : f.obj X ⟶ f.obj X),
  (hf.mulEquivEnd X).symm f_1 = hf.preimage f_1