-- Module: Mathlib.Topology.Category.LightProfinite.Limits
Goal:
X Y Z : LightProfinite
f : X ⟶ Z
g : Y ⟶ Z
h :
  Function.Surjective (α :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      Y)
    (β :=
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      Z)
    (⇑(ConcreteCategory.hom (FC :=
          fun
            (x1 x2 :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1)))
          (CC :=
          fun
            (X :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
          g) :
      (a :
          (fun
                (X :
                  CompHausLike fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
              (↑X.toTop : Type u_1))
            Y) →
        (fun
              (X :
                CompHausLike fun (X : TopCat) ↦
                  TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
            (↑X.toTop : Type u_1))
          Z)
x :
  (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
    Type u_1)
obtain :
  ∀
    (y :
      (↑(Y.toTop (P := fun (X : TopCat.{u_1}) ↦
            TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
        Type u_1))
    (hy :
      Eq (α :=
        (fun
              (X :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1))
          Z)
        ((ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1))
                g :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                      (↑X.toTop : Type u_1))
                    Y) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Z)
            y :
          (fun
                (X :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1))
            Z)
        ((ConcreteCategory.hom (FC :=
                fun
                  (x1 x2 :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                          SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                    Type u_1)))
                (CC :=
                fun
                  (X :
                    CompHausLike fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1))
                f :
              (a :
                  (fun
                        (X :
                          CompHausLike fun (X : TopCat) ↦
                            TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                      (↑X.toTop : Type u_1))
                    X) →
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  Z)
            x :
          (fun
                (X :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1))
            Z)),
    ∃ (a :
      (fun
            (X :
              CompHausLike fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
            Type u_1))
        (CompHausLike.pullback (P := fun (X : TopCat.{u_1}) ↦
          TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)),
      (ConcreteCategory.hom (FC :=
              fun
                (x1 x2 :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1),
                (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                      TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                  Type u_1)))
              (CC :=
              fun
                (X :
                  CompHausLike fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1))
              (X :=
              CompHausLike.pullback (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)
              (CompHausLike.pullback.fst (P := fun (X : TopCat.{u_1}) ↦
                TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g) :
            (a :
                (fun
                      (X :
                        CompHausLike fun (X : TopCat) ↦
                          TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                    (↑X.toTop : Type u_1))
                  (CompHausLike.pullback f g)) →
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                  (↑X.toTop : Type u_1))
                X)
          a =
        x
⊢ ∃ (a :
    (fun
          (X :
            CompHausLike fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
          Type u_1))
      (CompHausLike.pullback (P := fun (X : TopCat.{u_1}) ↦
        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)),
    (ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1),
              (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                    TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                Type u_1)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦
                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
              Type u_1))
            (X :=
            CompHausLike.pullback (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g)
            (CompHausLike.pullback.fst (P := fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1)) f g) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                  (↑X.toTop : Type u_1))
                (CompHausLike.pullback f g)) →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u_1) ∧ SecondCountableTopology (↑X : Type u_1)) ↦
                (↑X.toTop : Type u_1))
              X)
        a =
      x

Tactic:
obtain ⟨y, hy⟩ := h (f x)

Premises used: CategoryTheory.ConcreteCategory.hom, DFunLike.coe