∀ (X : Profinite) [inst : Finite ↑X.toTop] (t : CategoryTheory.Limits.Cofan fun x => Profinite.of PUnit.{u_1 + 1})
  (j : ↑X.toTop),
  CategoryTheory.CategoryStruct.comp ((Condensed.fintypeCatAsCofan X).inj j)
      ((fun t =>
          CategoryTheory.ConcreteCategory.ofHom
            { toFun := fun x => (CategoryTheory.ConcreteCategory.hom (t.inj x)) PUnit.unit, continuous_toFun := ⋯ })
        t) =
    t.inj j