-- Module: Mathlib.Condensed.Discrete.Colimit
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
fi :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{u} (↑X : Type u))) :
      Type u)
    X
fj :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop (P := fun (X : TopCat.{u}) ↦
          TotallyDisconnectedSpace.{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 : I
ki : k ⟶ i
kj : k ⟶ j
h_1 : True
x_1 :
  (↑((toProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
x :
  (↑((obj (obj (const I) c.pt) k).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) :
    Type u)
hx :
  (ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) (c.π.app k) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              (((const I).obj c.pt).obj k)) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
            ((F ⋙ toProfinite).obj k))
      x =
    x_1
refine_2 :
  Eq (α := X)
    ((fi : (a : (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))).toTop : Type u)) → X)
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                (c.π.app k ≫ (F ⋙ toProfinite).map ki) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (((const I).obj c.pt).obj k)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  ((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i))))
            x :
          (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
            ((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op i)))) :
      X)
    ((fj : (a : (↑((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))).toTop : Type u)) → X)
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                (c.π.app k ≫ (F ⋙ toProfinite).map kj) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (((const I).obj c.pt).obj k)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  ((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j))))
            x :
          (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
            ((F ⋙ toProfinite).obj (Opposite.unop (Opposite.op j)))) :
      X)
⊢ Eq (α := X)
    (((({
                  toFun :=
                    fun
                      (g :
                        LocallyConstant
                          (↑((toProfinite.obj (F.obj i)).toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u)
                          X) ↦
                    LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map ki)).hom) g } :
                (a : LocallyConstant (↑(toProfinite.obj (F.obj i)).toTop : Type u) X) →
                  LocallyConstant (↑(toProfinite.obj (F.obj k)).toTop : Type u) X)
              fi :
            LocallyConstant
              (↑((toProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)
              X) :
          (a : (↑(toProfinite.obj (F.obj k)).toTop : Type u)) → X)
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                (c.π.app k) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (((const I).obj c.pt).obj k)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  ((F ⋙ toProfinite).obj k))
            x :
          (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
            ((F ⋙ toProfinite).obj k)) :
      X)
    (((({
                  toFun :=
                    fun
                      (g :
                        LocallyConstant
                          (↑((toProfinite.obj (F.obj j)).toTop (P := fun (X : TopCat.{u}) ↦
                                TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                            Type u)
                          X) ↦
                    LocallyConstant.comap (TopCat.Hom.hom (toProfinite.map (F.map kj)).hom) g } :
                (a : LocallyConstant (↑(toProfinite.obj (F.obj j)).toTop : Type u) X) →
                  LocallyConstant (↑(toProfinite.obj (F.obj k)).toTop : Type u) X)
              fj :
            LocallyConstant
              (↑((toProfinite.obj (F.obj k)).toTop (P := fun (X : TopCat.{u}) ↦
                    TotallyDisconnectedSpace.{u} (↑X : Type u))) :
                Type u)
              X) :
          (a : (↑(toProfinite.obj (F.obj k)).toTop : Type u)) → X)
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                  (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
                (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
                (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
                (c.π.app k) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (((const I).obj c.pt).obj k)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  ((F ⋙ toProfinite).obj k))
            x :
          (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
            ((F ⋙ toProfinite).obj k)) :
      X)

Tactic:
change fi ((c.π.app k ≫ (F ⋙ toProfinite).map _) x) =
      fj ((c.π.app k ≫ (F ⋙ toProfinite).map _) x)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, CategoryTheory.Functor.comp, CategoryTheory.Functor.map, FintypeCat.toProfinite, CategoryTheory.CategoryStruct.comp, DFunLike.coe, CategoryTheory.NatTrans.app