-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : LightProfinite
F_1 F : LightProfiniteᵒᵖ ⥤ Type u
X : LightProfinite
inst :
  Finite.{u_1 + 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_1 :
  Cofan (C := LightProfinite)
    fun
      (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)) ↦
    LightProfinite.of PUnit.{u_1 + 1}
x_2 : (fintypeCatAsCofan X).pt ⟶ x_1.pt
h :
  ∀
    (j :
      (↑(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)),
    (fintypeCatAsCofan X).inj j ≫ x_2 = x_1.inj j
x :
  (↑((fintypeCatAsCofan X).pt.toTop (P := fun (X : TopCat.{u_1}) ↦
        TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
    Type u_1)
⊢ Eq (α :=
    (↑(x_1.pt.toTop (P := fun (X : TopCat.{u_1}) ↦
          TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
      Type u_1))
    ((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_2 :
          (a : (↑(fintypeCatAsCofan X).pt.toTop : Type u_1)) → (↑x_1.pt.toTop : Type u_1))
        x :
      (↑(x_1.pt.toTop (P := fun (X : TopCat.{u_1}) ↦
            TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
        Type u_1))
    ((@ConcreteCategory.hom _
            (CompHausLike.category fun (X : TopCat.{u_1}) ↦
              TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))
            (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)))
            (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))
            _ _ (fintypeCatAsCofan X).pt x_1.pt
            ((fun
                  (t :
                    Cofan (C := LightProfinite)
                      fun
                        (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)) ↦
                      LightProfinite.of PUnit.{u_1 + 1}) ↦
                (ConcreteCategory.ofHom (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))
                    {
                      toFun :=
                        fun
                          (x :
                            (↑((fintypeCatAsCofan X).pt.toTop (P := fun (X : TopCat.{u_1}) ↦
                                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧
                                    SecondCountableTopology.{u_1} (↑X : Type u_1))) :
                              Type u_1)) ↦
                        (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))
                              (t.inj x) :
                            (a :
                                (fun
                                      (X :
                                        CompHausLike fun (X : TopCat) ↦
                                          TotallyDisconnectedSpace (↑X : Type u_1) ∧
                                            SecondCountableTopology (↑X : Type u_1)) ↦
                                    (↑X.toTop : Type u_1))
                                  (LightProfinite.of PUnit.{u_1 + 1})) →
                              (fun
                                    (X :
                                      CompHausLike fun (X : TopCat) ↦
                                        TotallyDisconnectedSpace (↑X : Type u_1) ∧
                                          SecondCountableTopology (↑X : Type u_1)) ↦
                                  (↑X.toTop : Type u_1))
                                t.pt)
                          PUnit.unit,
                      continuous_toFun := ⋯ } :
                  (fintypeCatAsCofan X).pt ⟶ t.pt))
              x_1) :
          (a : (↑(fintypeCatAsCofan X).pt.toTop : Type u_1)) → (↑x_1.pt.toTop : Type u_1))
        x :
      (↑(x_1.pt.toTop (P := fun (X : TopCat.{u_1}) ↦
            TotallyDisconnectedSpace.{u_1} (↑X : Type u_1) ∧ SecondCountableTopology.{u_1} (↑X : Type u_1))) :
        Type u_1))

Tactic:
exact CategoryTheory.congr_fun (h x) _

Premises used: CategoryTheory.congr_fun