∀ (R : Type (u + 1)) [inst : Ring R] (M : CondensedMod R),
  [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M),
      (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M,
      CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M),
      CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite)
        ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M),
      ∀ (S : Profinite),
        Nonempty
          (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.val).mapCocone S.asLimitCone.op))].TFAE