∀ (C : Type w) [inst : CategoryTheory.Category.{u, w} C]
  [inst_1 : CategoryTheory.HasSheafify (CategoryTheory.coherentTopology LightProfinite) C] {X Y : C} (f : X ⟶ Y),
  (LightCondensed.discrete C).map f =
    (CategoryTheory.presheafToSheaf (CategoryTheory.coherentTopology LightProfinite) C).map
      ((CategoryTheory.Functor.const LightProfiniteᵒᵖ).map f)