∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_6} {Nₗ : Type u_11} {Pₗ : Type u_12} {Qₗ : Type u_13}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : AddCommMonoid Qₗ]
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
  (g : Pₗ ≃ₗ[R] Qₗ), Function.Surjective ⇑f → Function.Surjective ⇑(f.compr₂ ↑g)