-- 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 :
  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_1 : (fintypeCatAsCofan X).pt ⟶ x.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_1 = x.inj j
h₁ :
  ∀
    (x_2 :
      (↑((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.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_1 :
            (a : (↑(fintypeCatAsCofan X).pt.toTop : Type u_1)) → (↑x.pt.toTop : Type u_1))
          x_2 :
        (↑(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 _
              (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.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) :
            (a : (↑(fintypeCatAsCofan X).pt.toTop : Type u_1)) → (↑x.pt.toTop : Type u_1))
          x_2 :
        (↑(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))
⊢ x_1 =
    (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

Tactic:
ext x