-- 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)
⊢ ∀
    (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})
    (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 ≫
        (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))
          t =
      t.inj j

Tactic:
aesop