-- 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
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
refine_2 :
  ∀
    (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)
⊢ 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:
ext x