-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
I : Type u
inst : Category.{u, u} I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
X : Type (u + 1)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
refine_1 :
  ∀ (x : ((locallyConstantPresheaf X).mapCocone c.op).pt),
    ∃ (i : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)),
      x =
        (ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
            (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
              (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
          xi
refine_2 :
  ∀ (i j : Iᵒᵖ) (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i))
    (xj : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)),
    Eq (α := (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app i) :
              (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
                (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj i))
            xi :
          (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) i))
        ((ConcreteCategory.hom (FC := TypeCat.Fun) (((locallyConstantPresheaf X).mapCocone c.op).ι.app j) :
              (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)) →
                (fun (X : Type (u + 1)) ↦ X) (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj j))
            xj :
          (fun (X : Type (u + 1)) ↦ X) (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) j)) →
      ∃ (k : Iᵒᵖ) (f : i ⟶ k) (g : j ⟶ k),
        Eq (α := (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map f) :
                (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj i)) →
                  (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              xi :
            (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).map g) :
                (a : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj j)) →
                  (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              xj :
            (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
⊢ IsColimit ((locallyConstantPresheaf X).mapCocone c.op)

Tactic:
refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_

Premises used: CategoryTheory.Limits.Types.FilteredColimit.isColimitOf