-- 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
x : (Finset I)ᵒᵖ
s : Finset I
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))
have this : Eq (α := (↑C : Type u) → (↑(IndexFunctor.obj (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) : Type u))
  (Function.comp (β := (↑(π C fun (x : I) ↦ x ∈ s) : 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))
    (ProjRestrict C fun (x : I) ↦ x ∈ s))
  (⇑(IndexFunctor.π_app (X := fun (i : I) ↦ Bool) C fun (x : I) ↦ x ∈ s) :
    (a : (↑C : Type u)) → (↑(IndexFunctor.obj C fun (x : I) ↦ x ∈ s) : Type u))
Tactic: have : iso_map C (· ∈ s) ∘ ProjRestrict C (· ∈ s) = IndexFunctor.π_app C (· ∈ s) := by
        ext _ i; exact dif_pos i.prop