-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (hypothesis)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
h1 :
  ι ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x) =
    (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
      ((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))
          x :
        (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)))
          (F.obj j))
⊢ Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
    (if h :
          ∃ (a : α),
            ι a =
              (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
                ((TopCat.Hom.hom (C.π.app j).hom :
                      (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
                    x :
                  (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))) then
        h.choose (p := fun (a : α) ↦
          ι a =
            (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
              ((TopCat.Hom.hom (C.π.app j).hom :
                    (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
                  x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))))
      else default :
      α)
have h2 : ∃ (a : α),
  ι a =
    (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
      ((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))
          x :
        (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)))
          (F.obj j))
Tactic: have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩