-- Lean 4 proof step from Mathlib.Condensed.Discrete.Colimit (goal)
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
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
h :
  LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) fi = LocallyConstant.comap (TopCat.Hom.hom (c.π.app j).hom) fj
k : ℕᵒᵖ
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
⊢ Eq (α := (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map ki.op) :
          (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 (Opposite.op k)))
        fi :
      (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).map kj.op) :
          (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 (Opposite.op k)))
        fj :
      (fun (X : Type u) ↦ X) (((F ⋙ toLightProfinite).op ⋙ locallyConstantPresheaf X).obj (Opposite.op k)))
have refine_2 : Eq (α :=
  LocallyConstant
    (↑((toLightProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u)
    X)
  (({
          toFun :=
            fun
              (g :
                LocallyConstant
                  (↑((toLightProfinite.obj (F.obj i)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                    Type u)
                  X) ↦
            LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map ki)).hom) g } :
        (a : LocallyConstant (↑(toLightProfinite.obj (F.obj i)).toTop : Type u) X) →
          LocallyConstant (↑(toLightProfinite.obj (F.obj k)).toTop : Type u) X)
      fi :
    LocallyConstant
      (↑((toLightProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)
      X)
  (({
          toFun :=
            fun
              (g :
                LocallyConstant
                  (↑((toLightProfinite.obj (F.obj j)).toTop (P := fun (X : TopCat.{u}) ↦
                        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                    Type u)
                  X) ↦
            LocallyConstant.comap (TopCat.Hom.hom (toLightProfinite.map (F.map kj)).hom) g } :
        (a : LocallyConstant (↑(toLightProfinite.obj (F.obj j)).toTop : Type u) X) →
          LocallyConstant (↑(toLightProfinite.obj (F.obj k)).toTop : Type u) X)
      fj :
    LocallyConstant
      (↑((toLightProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
            TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
        Type u)
      X)
Tactic: dsimp