Balanced categories and functors reflecting isomorphisms

If a category is C, and a functor out of C reflects epimorphisms and monomorphisms, then the functor reflects isomorphisms. Furthermore, categories that admit a functor that ReflectsIsomorphisms, PreservesEpimorphisms and PreservesMonomorphisms are balanced.

@[instance 100]

instance CategoryTheory.reflectsIsomorphisms_of_reflectsMonomorphisms_of_reflectsEpimorphisms {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [Balanced C] (F : Functor C D) [F.ReflectsMonomorphisms] [F.ReflectsEpimorphisms] : F.ReflectsIsomorphisms

theorem CategoryTheory.Functor.balanced_of_preserves {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.ReflectsIsomorphisms] [F.PreservesEpimorphisms] [F.PreservesMonomorphisms] [Balanced D] : Balanced C