-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (goal)
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)
⊢ (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))) })
have 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))
                        sorry :
                      (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))
                        sorry :
                      (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))
Tactic: ext x