-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
this :
  DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
f' : LocallyConstant
  (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
    Type (max u w)) :=
  {
    toFun :=
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
                (↑X.toTop : Type (max u w)))
              c.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑X.toTop : Type (max u w)))
            (toProfinite.obj X)),
    isLocallyConstant := ⋯ }
i : I
g :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max w u)))) :
      Type (max w u))
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
h₁ :
  ∀ (x : (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))),
    Eq (α :=
      (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
        Type (max u w)))
      ((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
                (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
                  Type (max u w))))
              (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)))
              f :
            (a : (↑c.pt.toTop : Type (max u w))) → (↑(toProfinite.obj X).toTop : Type (max u w)))
          x :
        (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
          Type (max u w)))
      ((ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
                (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
                  Type (max u w))))
              (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)))
              (Y := toProfinite.obj X)
              (c.π.app i ≫
                toProfinite.map
                  (InducedCategory.Hom.mk (F := ObjectProperty.FullSubcategory.obj)
                    (↾(⇑g :
                        (a : (↑((F ⋙ toProfinite).obj i).toTop : Type (max w u))) →
                          (↑(toProfinite.obj X).toTop : Type (max u w)))))) :
            (a : (↑c.pt.toTop : Type (max u w))) → (↑(toProfinite.obj X).toTop : Type (max u w)))
          x :
        (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
          Type (max u w)))
⊢ f =
    c.π.app i ≫
      toProfinite.map
        (InducedCategory.Hom.mk (F := ObjectProperty.FullSubcategory.obj)
          (↾(⇑g :
              (a : (↑((F ⋙ toProfinite).obj i).toTop : Type (max w u))) →
                (↑(toProfinite.obj X).toTop : Type (max u w)))))

Tactic:
ext x