-- 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
x : (Finset I)ᵒᵖ
s : Finset I
h :
  ∀
    (a :
      (↑((Functor.obj
                (Functor.obj (Functor.const (Finset I)ᵒᵖ)
                  (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                    (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
                (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 s)).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 :=
              Functor.obj
                (Functor.obj (Functor.const (Finset I)ᵒᵖ)
                  (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                    (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
                (op s))
              (NatTrans.app (Cone.π (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)) (op s)) :
            (a : (↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop : Type u)) →
              (↑((indexFunctor hC).obj (op s)).toTop : Type u))
          a :
        (↑(((indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op s)).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 s))
              (Iso.hom
                  (Iso.refl
                    (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
                      (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC))) ≫
                (Functor.obj (C := Cone (spanFunctor (C := C) hC))
                        (Cone.postcompose (Iso.hom (spanFunctorIsoIndexFunctor (C := C) hC)))
                        (spanCone (C := C) hC)).π.app
                  (op s)) :
            (a : (↑(((Functor.const (Finset I)ᵒᵖ).obj (indexCone hC).pt).obj (op s)).toTop : Type u)) →
              (↑((indexFunctor hC).obj (op s)).toTop : Type u))
          a :
        (↑(((indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op s)).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u))
⊢ Eq (α :=
    Functor.obj
        (Functor.obj (Functor.const (Finset I)ᵒᵖ)
          (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
            (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)))
        (op s) ⟶
      (indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC).obj (op s))
    (NatTrans.app (Cone.π (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC)) (op s))
    (Iso.hom
        (Iso.refl
          (Cone.pt (F := indexFunctor (X := fun (i : I) ↦ Bool) (C := C) hC)
            (indexCone (X := fun (i : I) ↦ Bool) (C := C) hC))) ≫
      (Functor.obj (C := Cone (spanFunctor (C := C) hC))
              (Cone.postcompose (Iso.hom (spanFunctorIsoIndexFunctor (C := C) hC))) (spanCone (C := C) hC)).π.app
        (op s))

Tactic:
ext