-- 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)
i j : I
fi :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
refine_2 :
  ∀ (k : I) (ki : k ⟶ i) (kj : k ⟶ j),
    True →
      ∃ (k : Iᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op 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 (Opposite.op i))) →
                  (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              fi :
            (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 (Opposite.op j))) →
                  (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              fj :
            (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
⊢ ∃ (k : Iᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op 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 (Opposite.op i))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fi :
        (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 (Opposite.op j))) →
              (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          fj :
        (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j

Premises used: CategoryTheory.IsCofilteredOrEmpty.cone_objs