∀ {R : Type u_1} [inst : CommRing R] {M1 : Type u_2} {M2 : Type u_3} {M3 : Type u_4} (N : Type u_5)
  [inst_1 : AddCommGroup M1] [inst_2 : AddCommGroup M2] [inst_3 : AddCommGroup M3] [inst_4 : AddCommGroup N]
  [inst_5 : Module R M1] [inst_6 : Module R M2] [inst_7 : Module R M3] [inst_8 : Module R N] {f : M1 →ₗ[R] M2}
  {g : M2 →ₗ[R] M3},
  Function.Exact ⇑f ⇑g → Function.Surjective ⇑g → Function.Exact ⇑(LinearMap.lcomp R N g) ⇑(LinearMap.lcomp R N f)