CategoryTheory.isIso_of_mono_of_epi

theorem CategoryTheory.isIso_of_mono_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Balanced C] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f] [inst_3 : CategoryTheory.Epi f], CategoryTheory.IsIso f

This theorem states that in any balanced category `C`, for any objects `X` and `Y` in `C`, if `f` is a morphism from `X` to `Y` which is both a monomorphism (i.e., left-cancellable) and an epimorphism (i.e., right-cancellable), then `f` is an isomorphism. A balanced category is one in which every morphism that is both a monomorphism and an epimorphism is an isomorphism. Thus, the theorem essentially asserts that the definition of a balanced category is upheld for any given pair of objects and morphism in that category.

More concisely: In a balanced category, any morphism that is both a monomorphism and an epimorphism is an isomorphism.