∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M₀ : Type u_2} {M₀' : Type u_5} [inst_1 : AddCommMonoid M₀]
  [inst_2 : AddCommMonoid M₀'] [inst_3 : Module R M₀] [inst_4 : Module R M₀'] (f₀ : M₀ →ₗ[R] M₀')
  [inst_5 : IsLocalizedModule S f₀] {M₁ : Type u_3} {M₁' : Type u_6} [inst_6 : AddCommMonoid M₁]
  [inst_7 : AddCommMonoid M₁'] [inst_8 : Module R M₁] [inst_9 : Module R M₁'] (f₁ : M₁ →ₗ[R] M₁')
  [inst_10 : IsLocalizedModule S f₁] {M₂ : Type u_4} {M₂' : Type u_7} [inst_11 : AddCommMonoid M₂]
  [inst_12 : AddCommMonoid M₂'] [inst_13 : Module R M₂] [inst_14 : Module R M₂'] (f₂ : M₂ →ₗ[R] M₂')
  [inst_15 : IsLocalizedModule S f₂] (g : M₀ →ₗ[R] M₁) (h : M₁ →ₗ[R] M₂),
  Function.Exact ⇑g ⇑h → Function.Exact ⇑((IsLocalizedModule.map S f₀ f₁) g) ⇑((IsLocalizedModule.map S f₁ f₂) h)