-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Nobeling.Basic (hypothesis)
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)
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))
have this : Eq (α :=
  (↑(π C (Membership.mem (unop (op s)))) : Type u) →
    (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ t) : Type u))
  (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ t) : Type u))
    (⇑(iso_map C fun (x : I) ↦ x ∈ t) :
      (a : (↑(π C fun (x : I) ↦ x ∈ t) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ t) : Type u))
    (ProjRestricts C (J := fun (x : I) ↦ x ∈ t) (K := Membership.mem (unop (op s))) f))
  (Function.comp (β := (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C (Membership.mem (unop (op s)))) : Type u))
    (⇑(IndexFunctor.map (X := fun (i : I) ↦ Bool) C (J := Membership.mem (unop (op t))) (K :=
          Membership.mem (unop (op s))) f) :
      (a : (↑(IndexFunctor.obj C (Membership.mem (unop (op s)))) : Type u)) →
        (↑(IndexFunctor.obj C (Membership.mem (unop (op t)))) : Type u))
    (⇑(iso_map C fun (x : I) ↦ x ∈ s) :
      (a : (↑(π C fun (x : I) ↦ x ∈ s) : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u)))
Tactic: have : iso_map C (· ∈ t) ∘ ProjRestricts C f =
            IndexFunctor.map C f ∘ iso_map C (· ∈ s) := by
          ext _ i; exact dif_pos i.prop