-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
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))
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))
h₁ :
  (f : (a : (↑C.pt.toTop : Type (max u v))) → α) x =
    h2.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))))
⊢ 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 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)))
Tactic: rw [dif_pos]