∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [(CategoryTheory.forget₂ C Ab).PreservesHomology]
  [CategoryTheory.Limits.HasZeroObject C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Mono f ↔
    Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map f))