-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
            (C.π.app j)) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑X.toTop : Type (max u v)))
              (((Functor.const J).obj C.pt).obj j)) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
              (↑X.toTop : Type (max u v)))
            (F.obj j)) ⁻¹'
      V
w : J
w₁ :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2)
h₁ h₂ : f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)
h₃ :
  Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    (Set.preimage (β := Fin 2)
      (⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)) :
        (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
      {0})
h₄ :
  Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    ((⇑(TopCat.Hom.hom (C.π.app j).hom) :
        (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) ⁻¹'
      V)
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
classical
  use j, LocallyConstant.ofIsClopen hV
  apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
  simp only [Fin.isValue, Functor.const_obj_obj, LocallyConstant.coe_comap, Set.preimage_comp,
    LocallyConstant.ofIsClopen_fiber_zero]
  exact h

Premises used: LocallyConstant.locallyConstant_eq_of_fiber_zero_eq, LocallyConstant.ofIsClopen_fiber_zero, LocallyConstant.coe_comap, Set.preimage_comp, Fin.isValue, CategoryTheory.Functor.const_obj_obj