-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
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
⊢ 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)))))
have 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)))
Tactic: ext x