theorem corollary_23_60 {R : Type u} [CommRing R] {M₁ M₂ M₃ : Type u} [AddCommGroup M₁] [AddCommGroup M₂] [AddCommGroup M₃] [Module R M₁] [Module R M₂] [Module R M₃] (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (_hf : Function.Injective ⇑f) (hfg : Function.Exact ⇑f ⇑g) (hg : Function.Surjective ⇑g) (A : Type u) [AddCommGroup A] [Module R A] : Function.Injective ⇑(LinearMap.lcomp R A g) ∧ Function.Exact ⇑(LinearMap.lcomp R A g) ⇑(LinearMap.lcomp R A f)