∀ (R : Type u) [inst : Ring R] {X Y : LightCondMod R} (f : X ⟶ Y) [CategoryTheory.Epi f] {S : LightProfinite}
  (p : (LightCondensed.free R).obj S.toCondensed ⟶ Y),
  ∃ T π g,
    CategoryTheory.Epi π ∧
      CategoryTheory.CategoryStruct.comp ((lightProfiniteToLightCondSet.comp (LightCondensed.free R)).map π) p =
        CategoryTheory.CategoryStruct.comp g f