∀ {R : Type u_2} {M : Type u_4} {K : Type u_6} {P : Type u_1} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup K] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R K] [inst_6 : Module R P]
  {f : K →ₗ[R] M} {g : M →ₗ[R] P} {s : M →ₗ[R] K},
  s ∘ₗ f = LinearMap.id →
    Function.Exact ⇑f ⇑g →
      ∀ {ι : Type u_5} {κ : Type u_3} {σ : Type u_7} {a : κ → ι} {b : σ → ι},
        Function.Surjective ⇑g →
          ∀ (v : Module.Basis ι R M),
            (∀ (i : κ), s (v (a i)) = 0) →
              LinearIndependent R (⇑s ∘ ⇑v ∘ b) →
                Codisjoint (Set.range a) (Set.range b) → ⊤ ≤ Submodule.span R (Set.range (⇑g ∘ ⇑v ∘ a))