-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X : CompHaus
Y : Profinite
f : X.toProfiniteObj ⟶ Y
y : (↑(X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
obtain :
  ∀ (y : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
    Eq (α := (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
              TopCat.carrier _ _
              (X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
              (Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
              (InducedCategory.Hom.hom
                ((fun (g : X ⟶ profiniteToCompHaus.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 := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
                          C((↑(X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦
                                  TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u),
                            (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u)) } :
                      X.toProfiniteObj ⟶ Y))
                  ((fun (f : X.toProfiniteObj ⟶ Y) ↦
                      (ofHom (fun (x : TopCat.{u}) ↦ True)
                          ((TopCat.Hom.hom f.hom).comp { toFun := Quotient.mk'', continuous_toFun := ⋯ }) :
                        Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                          (CompHausLike.of (fun (x : TopCat.{u}) ↦ True) (↑X.1 : Type u))
                          (CompHausLike.of (fun (x : TopCat.{u}) ↦ True)
                            (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                              Type u))))
                    f))) :
            (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
          (ConnectedComponents.mk y) :
        (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              f.hom :
            (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
          (ConnectedComponents.mk y) :
        (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
⊢ Eq (α := (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((@ConcreteCategory.hom _ TopCat.instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            TopCat.carrier _ _
            (X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
            (Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)))
            (InducedCategory.Hom.hom
              ((fun (g : X ⟶ profiniteToCompHaus.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 := ⋯.connectedComponentsLift, continuous_toFun := ⋯ :
                        C((↑(X.toProfiniteObj.toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u),
                          (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u)) } :
                    X.toProfiniteObj ⟶ Y))
                ((fun (f : X.toProfiniteObj ⟶ Y) ↦
                    (ofHom (fun (x : TopCat.{u}) ↦ True)
                        ((TopCat.Hom.hom f.hom).comp { toFun := Quotient.mk'', continuous_toFun := ⋯ }) :
                      Quiver.Hom (V := CompHausLike fun (x : TopCat.{u}) ↦ True)
                        (CompHausLike.of (fun (x : TopCat.{u}) ↦ True) (↑X.1 : Type u))
                        (CompHausLike.of (fun (x : TopCat.{u}) ↦ True)
                          (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u))))
                  f))) :
          (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
        y :
      (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            f.hom :
          (a : (↑X.toProfiniteObj.toTop : Type u)) → (↑Y.toTop : Type u))
        y :
      (↑(Y.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))

Tactic:
obtain ⟨y, rfl⟩ := ConnectedComponents.surjective_coe y

Premises used: ConnectedComponents.surjective_coe, rfl