CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono

theorem CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C] {R₁ R₂ : CategoryTheory.ComposableArrows C 4}, R₁.Exact → R₂.Exact → ∀ (φ : R₁ ⟶ R₂), CategoryTheory.Epi (CategoryTheory.ComposableArrows.app' φ 0 ⋯) → CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 1 ⋯) → CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 3 ⋯) → CategoryTheory.Mono (CategoryTheory.ComposableArrows.app' φ 4 ⋯) → CategoryTheory.IsIso (CategoryTheory.ComposableArrows.app' φ 2 ⋯)

This theorem is the Lean 4 version of the Five Lemma from homological algebra. The Five Lemma states that, given two exact sequences of composable arrows in an Abelian category, if the maps at positions 0 and 4 are epi and mono respectively, and the maps at positions 1 and 3 are isomorphisms, then the map at position 2 is also an isomorphism. Here, `R₁` and `R₂` are two sequences of composable arrows in the category `C`. The function `CategoryTheory.ComposableArrows.app' φ i` refers to the `i`-th map of the morphism `φ` from `R₁` to `R₂`. The attribute `Exact` guarantees that the sequences `R₁` and `R₂` are exact.

More concisely: If in an Abelian category, sequences `R₁` and `R₂` of composable arrows are exact and the maps at positions 0 and 4 are epic and monic respectively, with the maps at positions 1 and 3 being isomorphisms, then the map at position 2 is also an isomorphism.