-- 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
x :
  (↑((toLightProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
        TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
    Type u)
⊢ Eq (α := 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) :
          (a : (↑(toLightProfinite.obj (F.obj k)).toTop : Type u)) → X)
        x :
      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) :
          (a : (↑(toLightProfinite.obj (F.obj k)).toTop : Type u)) → X)
        x :
      X)
have refine_2 : ∀
  (x_1 :
    (↑((obj (obj (const ℕᵒᵖ) c.pt) k).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
      Type u))
  (hx :
    (ConcreteCategory.hom (FC :=
            fun
              (x1 x2 :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
                Type u)))
            (CC :=
            fun
              (X :
                CompHausLike fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦
                  TotallyDisconnectedSpace.{u} (↑X : Type u) ∧ SecondCountableTopology.{u} (↑X : Type u))) :
              Type u))
            (c.π.app k) :
          (a :
              (fun
                    (X :
                      CompHausLike fun (X : TopCat) ↦
                        TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                  (↑X.toTop : Type u))
                (((const ℕᵒᵖ).obj c.pt).obj k)) →
            (fun
                  (X :
                    CompHausLike fun (X : TopCat) ↦
                      TotallyDisconnectedSpace (↑X : Type u) ∧ SecondCountableTopology (↑X : Type u)) ↦
                (↑X.toTop : Type u))
              ((F ⋙ toLightProfinite).obj k))
        x_1 =
      x),
  Eq (α := 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) :
          (a : (↑(toLightProfinite.obj (F.obj k)).toTop : Type u)) → X)
        x :
      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) :
          (a : (↑(toLightProfinite.obj (F.obj k)).toTop : Type u)) → X)
        x :
      X)
Tactic: obtain ⟨x, hx⟩ := ((LightProfinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x