theorem CategoryTheory.Lemma_2_7_1 {C : Type u₁} [Category.{v₁, u₁} C] [MonoidalCategory C] {M : Type u₂} [Category.{v₂, u₂} M] [ExactModuleCategory C M] [EnoughProjectives C] (hEpi : ∀ {X Y : C} (f : X ⟶ Y) (N : M), Epi f → Epi (LeftModuleCategoryStruct.actWhiskerRight f N)) : EnoughProjectives M

Lemma 2.7.1 (EGNO): If C has enough projectives and the action preserves epis on the first variable, then any exact module category over C also has enough projectives.