-- Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic
Goal:
I : Type u
C : Set (I → Bool)
J K L : I → Prop
inst : (i : I) → Decidable (J i)
inst_1 : (i : I) → Decidable (K i)
inst_2 : (i : I) → Decidable (L i)
inst_3 : (s : Finset I) → (i : I) → Decidable (i ∈ s)
hC : IsCompact C
s t : Finset I
f : unop (op t) ≤ unop (op s)
h :
  ∀
    (x :
      (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)),
    Eq (α :=
      (↑(((indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op t)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u))
      ((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (Y :=
              (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op t))
              ((spanFunctor (C := C) hC).map
                  (op
                    { down := { down := f : PLift (unop (op t) ≤ unop (op s)) } :
                      ULift.{u, 0} (PLift (unop (op t) ≤ unop (op s))) }) ≫
                Iso.hom
                  ((fun (s : (Finset I)ᵒᵖ) ↦
                      (CompHausLike.isoOfBijective (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u))
                          (ConcreteCategory.ofHom (FC :=
                            fun
                              (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u),
                              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u)))
                            (CC :=
                            fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u))
                            (iso_map C fun (x : I) ↦ x ∈ unop s))
                          ⋯ :
                        (spanFunctor (C := C) hC).obj s ≅ (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj s))
                    (op t))) :
            (a : (↑((spanFunctor hC).obj (op s)).toTop : Type u)) → (↑((indexFunctor hC).obj (op t)).toTop : Type u))
          x :
        (↑(((indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op t)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
      ((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (X :=
              (spanFunctor (C := C) hC).obj (op s))
              (Iso.hom
                  ((fun (s : (Finset I)ᵒᵖ) ↦
                      (CompHausLike.isoOfBijective (P := fun (X : TopCat.{u}) ↦
                          TotallyDisconnectedSpace.{u} (↑X : Type u))
                          (ConcreteCategory.ofHom (FC :=
                            fun
                              (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u),
                              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                                Type u)))
                            (CC :=
                            fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u))
                            (iso_map C fun (x : I) ↦ x ∈ unop s))
                          ⋯ :
                        (spanFunctor (C := C) hC).obj s ≅ (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj s))
                    (op s)) ≫
                (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).map
                  (op
                    { down := { down := f : PLift (unop (op t) ≤ unop (op s)) } :
                      ULift.{u, 0} (PLift (unop (op t) ≤ unop (op s))) })) :
            (a : (↑((spanFunctor hC).obj (op s)).toTop : Type u)) → (↑((indexFunctor hC).obj (op t)).toTop : Type u))
          x :
        (↑(((indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op t)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
⊢ (spanFunctor (C := C) hC).map
        (op
          { down := { down := f : PLift (unop (op t) ≤ unop (op s)) } :
            ULift.{u, 0} (PLift (unop (op t) ≤ unop (op s))) }) ≫
      Iso.hom
        ((fun (s : (Finset I)ᵒᵖ) ↦
            (CompHausLike.isoOfBijective (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
                (ConcreteCategory.ofHom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                    (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                  (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                  (iso_map C fun (x : I) ↦ x ∈ unop s))
                ⋯ :
              (spanFunctor (C := C) hC).obj s ≅ (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj s))
          (op t)) =
    Iso.hom
        ((fun (s : (Finset I)ᵒᵖ) ↦
            (CompHausLike.isoOfBijective (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))
                (ConcreteCategory.ofHom (FC :=
                  fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                    (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                  (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                  (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                  (iso_map C fun (x : I) ↦ x ∈ unop s))
                ⋯ :
              (spanFunctor (C := C) hC).obj s ≅ (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj s))
          (op s)) ≫
      (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).map
        (op
          { down := { down := f : PLift (unop (op t) ≤ unop (op s)) } :
            ULift.{u, 0} (PLift (unop (op t) ≤ unop (op s))) })

Tactic:
ext x