∀ {I : Type u_1} {C : Set (I → Bool)} [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C)
  {X Y : (Finset I)ᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp ((Profinite.NobelingProof.spanFunctor hC).map f)
      ((fun s =>
            CompHausLike.isoOfBijective
              (CategoryTheory.ConcreteCategory.ofHom (Profinite.NobelingProof.iso_map C fun x => x ∈ Opposite.unop s))
              ⋯)
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun s =>
            CompHausLike.isoOfBijective
              (CategoryTheory.ConcreteCategory.ofHom (Profinite.NobelingProof.iso_map C fun x => x ∈ Opposite.unop s))
              ⋯)
          X).hom
      ((Profinite.indexFunctor hC).map f)