-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
F : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts F
X Y : Profinite
inst_1 : Finite.{u + 1} (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
inst_2 : Finite.{u + 1} (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
f :
  (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →
    F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))
g : X ⟶ Y
⊢ Eq (α :=
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u) →
      F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
    (f ∘
      (⇑(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)) g) :
        (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
        (a : F.obj (Opposite.op X)) → (↑X.toTop : Type u) → F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) : (a : F.obj (Opposite.op Y)) → F.obj (Opposite.op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F Y).inv :
              (a : (↑Y.toTop : Type u) → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) → F.obj (Opposite.op Y))
            f) :
        F.obj (Opposite.op X)))
have a : ∀ (x : (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
  (f ∘
        (⇑(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)) g) :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u)))
      x =
    (ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F X).hom :
        (a : F.obj (Opposite.op X)) → (↑X.toTop : Type u) → F.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (F.map g.op) : (a : F.obj (Opposite.op Y)) → F.obj (Opposite.op X))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (isoFinYonedaComponents F Y).inv :
              (a : (↑Y.toTop : Type u) → F.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) → F.obj (Opposite.op Y))
            f) :
        F.obj (Opposite.op X))
      x
Tactic: ext x