∀ (R : Type u) [inst : Ring R] (M : LightCondMod R),
  [LightCondensed.IsDiscrete M,
      CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M),
      ∀ (S : LightProfinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit
            (M.val.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE