-- 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
x : (Finset I)ᵒᵖ
s : Finset I
⊢ 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))
have 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))
Tactic: ext