Lean4
/-- The condensed object associated to a presheaf on `Profinite` whose postcomposition with the
forgetful functor preserves finite products and satisfies the equalizer condition.
-/
noncomputable def ofSheafForgetProfinite [∀ X, HasLimitsOfShape (StructuredArrow X profiniteToCompHaus.op) A]
[HasForget A] [ReflectsFiniteLimits (CategoryTheory.forget A)] (F : Profinite.{u}ᵒᵖ ⥤ A)
[PreservesFiniteProducts (F ⋙ CategoryTheory.forget A)] (hF : EqualizerCondition (F ⋙ CategoryTheory.forget A)) :
Condensed A :=
ProfiniteCompHaus.equivalence A |>.functor.obj
{ val := F
cond := by
apply isSheaf_coherent_of_hasPullbacks_of_comp F (CategoryTheory.forget A)
rw [isSheaf_iff_preservesFiniteProducts_and_equalizerCondition]
exact ⟨⟨fun _ ↦ inferInstance⟩, hF⟩ }
