-- 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 α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Eq (α := Fin 2)
    ((LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) :
          (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
        x :
      Fin 2)
    ((g a : (a : (↑(F.obj (j a)).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 j0 ≫ F.map (fs a)) :
            (a_1 :
                (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 j0)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                  (↑X.toTop : Type (max u v)))
                (F.obj (j a)))
          x) :
      Fin 2)
have intro : Eq (α := Fin 2)
  ((LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) :
        (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
      x :
    Fin 2)
  ((g a : (a : (↑(F.obj (j a)).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)))
              (X := Functor.obj (Functor.obj (Functor.const J) C.pt) j0) (C.π.app (j a)) :
            C((↑((Functor.obj (Functor.obj (Functor.const J) C.pt) j0).toTop (P := fun (X : TopCat) ↦
                    TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v)),
              (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v)))) :
          (a_1 :
              (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 j0)) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑X.toTop : Type (max u v)))
              (F.obj (j a)))
        x) :
    Fin 2)
Tactic: rw [C.w]