∀ {F G : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (S : LightProfiniteᵒᵖ)
  (i : FintypeCat.toLightProfinite.op.comp F ≅ FintypeCat.toLightProfinite.op.comp G),
  (LightCondensed.lanPresheafExt i).hom.app S =
    CategoryTheory.Limits.colimMap
      ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op S).whiskerLeft i.hom)