-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
S : Profinite
F_1 F : Profiniteᵒᵖ ⥤ Type (u + 1)
X : Profinite
inst :
  Finite.{u_1 + 1}
    (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)
⊢ ∀
    (t :
      Cofan (C := Profinite)
        fun
          (x : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)) ↦
        Profinite.of PUnit.{u_1 + 1})
    (j : (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)),
    (fintypeCatAsCofan X).inj j ≫
        (fun
              (t :
                Cofan (C := Profinite)
                  fun
                    (x :
                      (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
                        Type u_1)) ↦
                  Profinite.of PUnit.{u_1 + 1}) ↦
            (ConcreteCategory.ofHom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
                    Type u_1),
                  (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{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)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{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))) :
                          Type u_1)) ↦
                    (ConcreteCategory.hom (FC :=
                          fun
                            (x1 x2 :
                              CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
                          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦
                                  TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
                              Type u_1),
                            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦
                                  TotallyDisconnectedSpace.{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)) ↦
                          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) :
                            Type u_1))
                          (t.inj x) :
                        (a :
                            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦
                                (↑X.toTop : Type u_1))
                              (Profinite.of PUnit.{u_1 + 1})) →
                          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑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