(R : Type (u + 1)) →
  [inst : Ring R] →
    (F : CategoryTheory.Functor Profiniteᵒᵖ (ModuleCat R)) →
      [CategoryTheory.Limits.PreservesFiniteProducts F] →
        CategoryTheory.regularTopology.EqualizerCondition F → CondensedMod R