∀ (α : Type u_1) {X Y : Set α} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (({ obj := fun s => CategoryTheory.MonoOver.mk Subtype.val,
                map := fun {s t} b => CategoryTheory.MonoOver.homMk (fun w => ⟨↑w, ⋯⟩) ⋯, map_id := ⋯,
                map_comp := ⋯ }.comp
            { obj := fun f => Set.range f.obj.hom, map := fun {f g} t => CategoryTheory.homOfLE ⋯, map_id := ⋯,
              map_comp := ⋯ }).map
        f)
      ((fun x => CategoryTheory.eqToIso ⋯) Y).hom =
    CategoryTheory.CategoryStruct.comp ((fun x => CategoryTheory.eqToIso ⋯) X).hom
      ((CategoryTheory.Functor.id (Set α)).map f)