-- Module: Mathlib.Condensed.Discrete.Colimit
Goal:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
X : Type u
hc : IsLimit c
inst : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
i j : ℕᵒᵖ
fi :
  LocallyConstant
    (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X
refine_2 :
  ∀
    (fj :
      LocallyConstant
        (↑(((F ⋙ toLightProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
              TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
          Type u)
        X),
    Eq (α :=
        (fun (X : Type u) ↦ X)
          (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
                (fun (X : Type u) ↦ X)
                  (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op i)))
            fi :
          (fun (X : Type u) ↦ X)
            (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
                (fun (X : Type u) ↦ X)
                  (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op j)))
            fj :
          (fun (X : Type u) ↦ X)
            (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op j))) →
      ∃ (k : ℕᵒᵖᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
        Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
                  (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              fi :
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
                  (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              fj :
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
⊢ ∀ (xj : (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    Eq (α :=
        (fun (X : Type u) ↦ X)
          (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op i)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
                (fun (X : Type u) ↦ X)
                  (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op i)))
            fi :
          (fun (X : Type u) ↦ X)
            (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op i)))
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (((locallyConstantPresheaf X).mapCocone c.op).ι.app (Opposite.op j)) :
              (a :
                  (fun (X : Type u) ↦ X)
                    (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
                (fun (X : Type u) ↦ X)
                  (((const ℕᵒᵖᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op j)))
            xj :
          (fun (X : Type u) ↦ X)
            (obj (obj (const ℕᵒᵖᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op j))) →
      ∃ (k : ℕᵒᵖᵒᵖ) (f : Opposite.op i ⟶ k) (g : Opposite.op j ⟶ k),
        Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map f) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
                  (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              fi :
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
          ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map g) :
                (a :
                    (fun (X : Type u) ↦ X)
                      (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
                  (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))
              xj :
            (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj k))

Tactic:
(fj : LocallyConstant _ _)