Lean4
/-- The functor `locallyConstantPresheaf` takes cofiltered limits of finite sets with surjective
projection maps to colimits.
-/
noncomputable def isColimitLocallyConstantPresheaf (hc : IsLimit c) [∀ i, Epi (c.π.app i)] :
IsColimit <| (locallyConstantPresheaf X).mapCocone c.op :=
by
refine Types.FilteredColimit.isColimitOf _ _ ?_ ?_
· intro (f : LocallyConstant c.pt X)
obtain ⟨j, h⟩ := Profinite.exists_locallyConstant.{_, u} c hc f
exact ⟨⟨j⟩, h⟩
· intro ⟨i⟩ ⟨j⟩ (fi : LocallyConstant _ _) (fj : LocallyConstant _ _)
(h : fi.comap (c.π.app i).hom = fj.comap (c.π.app j).hom)
obtain ⟨k, ki, kj, _⟩ := IsCofilteredOrEmpty.cone_objs i j
refine ⟨⟨k⟩, ki.op, kj.op, ?_⟩
dsimp
ext x
obtain ⟨x, hx⟩ := ((Profinite.epi_iff_surjective (c.π.app k)).mp inferInstance) x
rw [← hx]
change fi ((c.π.app k ≫ (F ⋙ toProfinite).map _) x) = fj ((c.π.app k ≫ (F ⋙ toProfinite).map _) x)
have h := LocallyConstant.congr_fun h x
rwa [c.w, c.w]
