∀ {I : Type u_1} {C : Set (I → Bool)} [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C)
  {X Y Z : (Finset I)ᵒᵖ} (x : X ⟶ Y) (x_1 : Y ⟶ Z),
  CompHausLike.ofHom (fun X => TotallyDisconnectedSpace ↑X)
      { toFun := Profinite.NobelingProof.ProjRestricts C ⋯, continuous_toFun := ⋯ } =
    CategoryTheory.CategoryStruct.comp
      (CompHausLike.ofHom (fun X => TotallyDisconnectedSpace ↑X)
        { toFun := Profinite.NobelingProof.ProjRestricts C ⋯, continuous_toFun := ⋯ })
      (CompHausLike.ofHom (fun X => TotallyDisconnectedSpace ↑X)
        { toFun := Profinite.NobelingProof.ProjRestricts C ⋯, continuous_toFun := ⋯ })