-- 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 Y : (Finset I)ᵒᵖ
h : X ⟶ Y
simp :
  Eq (α := of (↑C : Type u) ⟶ (spanFunctor (C := C) hC).obj Y)
    (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))
      {
        toFun :=
          Function.comp (β := (↑(π C (Membership.mem (unop X))) : Type u))
            (ProjRestricts C (J := Membership.mem (unop Y)) (K := Membership.mem (unop X)) ⋯)
            (ProjRestrict C (Membership.mem (unop X))),
        continuous_toFun := ⋯ })
    (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))
        { toFun := ProjRestrict C fun (x : I) ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
      (spanFunctor (C := C) hC).map h)
⊢ Eq (α :=
    Functor.obj (Functor.obj (Functor.const (Finset I)ᵒᵖ) (of (↑C : Type u))) X ⟶ (spanFunctor (C := C) hC).obj Y)
    (CategoryTheory.Functor.map (Functor.obj (Functor.const (Finset I)ᵒᵖ) (of (↑C : Type u))) h ≫
      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))
        { toFun := ProjRestrict C fun (x : I) ↦ x ∈ unop Y, continuous_toFun := ⋯ })
    (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))
        { toFun := ProjRestrict C fun (x : I) ↦ x ∈ unop X, continuous_toFun := ⋯ } ≫
      (spanFunctor (C := C) hC).map h)

Tactic:
simp only [Functor.const_obj_obj,
        Functor.const_obj_map, Category.id_comp, ← projRestricts_comp_projRestrict C
        (leOfHom h.unop)]

Premises used: Profinite.NobelingProof.projRestricts_comp_projRestrict, Quiver.Hom.unop, CategoryTheory.Functor.const_obj_obj, CategoryTheory.leOfHom, CategoryTheory.Functor.const_obj_map, CategoryTheory.Category.id_comp