theorem lemma_23_58 {R : Type u} [CommRing R] {M N P : Type u} [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] (φ : M →ₗ[R] N) (ψ : N →ₗ[R] P) : Function.Exact ⇑φ ⇑ψ ∧ Function.Surjective ⇑ψ ↔ ∀ (D : Type u) [inst : AddCommGroup D] [inst_1 : Module R D], Function.Injective ⇑(LinearMap.lcomp R D ψ) ∧ Function.Exact ⇑(LinearMap.lcomp R D ψ) ⇑(LinearMap.lcomp R D φ)