-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
Goal:
X : Profiniteᵒᵖ ⥤ Type (u + 1)
inst : PreservesFiniteProducts X
hX : (S : Profinite.{u}) → IsColimit (X.mapCocone S.asLimitCone.op)
S : Profiniteᵒᵖ
Y : FintypeCatᵒᵖ
right : Discrete PUnit.{1}
g : toProfinite.op.obj Y ⟶ obj (fromPUnit S) right
f :
  LocallyConstant
    (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    (X.obj
      (Opposite.op (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})))
x :
  Function.Fiber (Y :=
    (↑((toProfinite.obj (Opposite.unop Y)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u))
    (Z :=
    X.obj
      (Opposite.op (CompHausLike.of (fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) PUnit.{u + 1})))
    (⇑f :
      (a : (↑(toProfinite.obj (Opposite.unop Y)).toTop : Type u)) →
        X.obj (Opposite.op (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1})))
this :
  Finite.{u + 1}
    (↑((fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x).toTop (P :=
          fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
⊢ Eq (α := X.obj (Opposite.op (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (sigmaIncl (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
          (a : X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj))) → X.obj (Opposite.op (fiber f x)))
        (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                (Iso.inv (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj))) :
              TypeCat.Fun ((Opposite.unop Y).obj → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
                (X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj)))) :
            (a : (Opposite.unop Y).obj → X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) →
              X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj)))
          (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) :
      X.obj (Opposite.op (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun)
            (X.map
              (Quiver.Hom.op
                (IsTerminal.from
                  (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u)))
                  (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x)))) :
          (a :
              X.obj
                (Opposite.op
                  (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1}))) →
            X.obj (Opposite.op (fiber f x)))
        (Function.Fiber.image
          (⇑f :
            (a : (Opposite.unop Y).obj) →
              X.obj
                (Opposite.op
                  (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1})))
          x) :
      X.obj (Opposite.op (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x)))
have w : Eq (α :=
  (fun (X : Type (u + 1)) ↦ X)
    ((↑((fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x).toTop (P :=
            fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u) →
      X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
            (isoFinYonedaComponents X
              (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
          (fun (X : Type (u + 1)) ↦ X)
            ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (sigmaIncl (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
            (a : X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj))) → X.obj (Opposite.op (fiber f x)))
          (((@ConcreteCategory.hom _ types TypeCat.Fun _ _ _ _ _
                  (Iso.inv (isoFinYonedaComponents X (Profinite.of (Opposite.unop Y).obj))) :
                TypeCat.Fun ((Opposite.unop Y).obj → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))
                  (X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj)))) :
              (a : (Opposite.unop Y).obj → X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))) →
                X.obj (Opposite.op (Profinite.of (Opposite.unop Y).obj)))
            (⇑f : (a : (Opposite.unop Y).obj) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1})))) :
        X.obj (Opposite.op (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
    (fun (X : Type (u + 1)) ↦ X)
      ((↑((fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x).toTop (P :=
              fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u) →
        X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
  ((ConcreteCategory.hom (FC := TypeCat.Fun)
          (Iso.hom
            (isoFinYonedaComponents X
              (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
        (a : (fun (X : Type (u + 1)) ↦ X) (X.obj (Opposite.op (fiber f x)))) →
          (fun (X : Type (u + 1)) ↦ X)
            ((↑(fiber f x).toTop : Type u) → X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
      ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (X.map
                (Quiver.Hom.op
                  (IsTerminal.from
                    (CompHausLike.isTerminalPUnit (P := fun (X : TopCat.{u}) ↦
                      TotallyDisconnectedSpace.{u} (↑X : Type u)))
                    (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x)))) :
            (a :
                X.obj
                  (Opposite.op
                    (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1}))) →
              X.obj (Opposite.op (fiber f x)))
          (Function.Fiber.image
            (⇑f :
              (a : (Opposite.unop Y).obj) →
                X.obj
                  (Opposite.op
                    (CompHausLike.of (fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) PUnit.{u + 1})))
            x) :
        X.obj (Opposite.op (fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x))) :
    (fun (X : Type (u + 1)) ↦ X)
      ((↑((fiber (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) f x).toTop (P :=
              fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
          Type u) →
        X.obj (Opposite.op (Profinite.of PUnit.{u + 1}))))
Tactic: apply injective_of_mono (isoFinYonedaComponents X (fiber.{u, u + 1} f x)).hom