∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] [Small.{v, u} R],
  (∀ {M N : Type v} [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : Module R M] [inst_7 : Module R N]
      (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g) →
    Module.Projective R P