∀ (R : Type u) [inst : CommRing R] (P : LightCondMod R),
  CategoryTheory.InternallyProjective P ↔
    ∀ {A B : LightCondMod R} (e : A ⟶ B) [CategoryTheory.Epi e] (S : LightProfinite)
      (g : CategoryTheory.MonoidalCategoryStruct.tensorObj P ((LightCondensed.free R).obj S.toCondensed) ⟶ B),
      ∃ S' π,
        ∃ (_ : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)),
          ∃ g',
            CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerLeft P
                  ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π))
                g =
              CategoryTheory.CategoryStruct.comp g' e