-- Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
theorem exists_locallyConstant {α : Type*} (hC : IsLimit C) (f : LocallyConstant C.pt α) :
    ∃ (j : J) (g : LocallyConstant (F.obj j) α), f = g.comap (C.π.app _).hom

Proof state:
case inr
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'

Result:
case inr.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g'
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
⊢ ∃ g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩

Result:
case refine_1
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
A : Set α
⊢ IsOpen ((fun a => hj.elim a) ⁻¹' A)

case refine_2
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toTop
j : J
hj : IsEmpty ↑(F.obj j).toTop
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) { toFun := fun a => hj.elim a, isLocallyConstant := ⋯ }

Proof state:
case inr.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g'
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }

Tactic:
ext1 t

Result:
case inr.intro.intro.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g'
t : ↑C.pt.toTop
⊢ f t = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }) t

Proof state:
case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toTop
this✝¹ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this✝ : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), CompactSpace ↑((F ⋙ toTopCat).obj j)
cond : Nonempty ↑(TopCat.limitCone (F ⋙ toTopCat)).pt
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
CD : (TopCat.limitCone (F ⋙ toTopCat)).pt ⟶ D.pt
⊢ Nonempty ↑C.pt.toTop

Tactic:
exact cond.map CD

Result:
no goals

Proof state:
case inr.intro.intro.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
t : ↑C.pt.toTop
hj : f' t = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g') t
⊢ f t = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }) t

Tactic:
dsimp at hj ⊢

Result:
case inr.intro.intro.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toTop) (Quotient S.toSetoid) := { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' : LocallyConstant (↑(F.obj j).toTop) (Quotient S.toSetoid)
t : ↑C.pt.toTop
hj : f' t = g' ((TopCat.Hom.hom (C.π.app j)) t)
⊢ f t = ff (g' ((TopCat.Hom.hom (C.π.app j)) t))

Proof state:
case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j, IsEmpty ↑(F.obj j).toTop

Tactic:
simp only [← not_nonempty_iff, ← not_forall]

Result:
case inl
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) α
S : DiscreteQuotient ↑C.pt.toTop := f.discreteQuotient
ff : Quotient S.toSetoid → α := ⇑f.lift
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ¬∀ (x : J), Nonempty ↑(F.obj x).toTop