∀ (R : Type (u_1 + 1)) [inst : Ring R] {X Y : ModuleCat R} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((CondensedMod.LocallyConstant.functor R).map f)
      ((fun M => (CondensedMod.LocallyConstant.functorIsoDiscreteComponents R M).symm) Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun M => (CondensedMod.LocallyConstant.functorIsoDiscreteComponents R M).symm) X).hom
      ((Condensed.discrete (ModuleCat R)).map f)