-- 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)
x :
  (↑(((spanFunctor (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
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)))
⊢ 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))

Tactic:
congr_fun this x

Premises used: Subtype.map, Set.Mem, setOf, congr_fun, Set.MapsTo.restrict