-- 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)
    (((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a :
          (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
        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)))
            (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)
Tactic: change _ = (g a) ((C.π.app j0 ≫ F.map (fs a)) x)