-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
⊢ ∀ (xi : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i)))
    (xj : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
    Eq (α :=
        (fun (X : Type (u + 1)) ↦ X)
          (obj (obj (const Iᵒᵖ) ((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 + 1)) ↦ X)
                    (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
                (fun (X : Type (u + 1)) ↦ X)
                  (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op i)))
            xi :
          (fun (X : Type (u + 1)) ↦ X)
            (obj (obj (const Iᵒᵖ) ((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 + 1)) ↦ X)
                    (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
                (fun (X : Type (u + 1)) ↦ X)
                  (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op j)))
            xj :
          (fun (X : Type (u + 1)) ↦ X)
            (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op j))) →
      ∃ (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))
              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 (Opposite.op 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))
have refine_2 : ∀
  (fi :
    LocallyConstant
      (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u))) :
        Type u)
      X)
  (xj : (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))),
  Eq (α :=
      (fun (X : Type (u + 1)) ↦ X)
        (obj (obj (const Iᵒᵖ) ((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 + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op i))) →
              (fun (X : Type (u + 1)) ↦ X)
                (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op i)))
          fi :
        (fun (X : Type (u + 1)) ↦ X)
          (obj (obj (const Iᵒᵖ) ((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 + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op j))) →
              (fun (X : Type (u + 1)) ↦ X)
                (((const Iᵒᵖ).obj ((locallyConstantPresheaf X).mapCocone c.op).pt).obj (Opposite.op j)))
          xj :
        (fun (X : Type (u + 1)) ↦ X)
          (obj (obj (const Iᵒᵖ) ((locallyConstantPresheaf X).mapCocone c.op).pt) (Opposite.op j))) →
    ∃ (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))
            xj :
          (fun (X : Type (u + 1)) ↦ X) (((F ⋙ toProfinite).op ⋙ locallyConstantPresheaf X).obj k))
Tactic: (fi : LocallyConstant _ _)