∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {L : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid L]
  [inst_6 : Module R L] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_7 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_8 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_9 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6)
      [inst_10 : (r : ↑s) → AddCommMonoid (Nₚ r)] [inst_11 : (r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r)
      [inst_12 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (Lₚ : ↑s → Type u_7)
      [inst_13 : (r : ↑s) → AddCommMonoid (Lₚ r)] [inst_14 : (r : ↑s) → Module R (Lₚ r)] (h : (r : ↑s) → L →ₗ[R] Lₚ r)
      [inst_15 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (h r)] (F : M →ₗ[R] N) (G : N →ₗ[R] L),
      (∀ (r : ↑s),
          Function.Exact ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)
            ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (g r) (h r)) G)) →
        Function.Exact ⇑F ⇑G