-- 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.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

Tactic:
refine ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩

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'
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) { toFun := ff ∘ ⇑g', isLocallyConstant := ⋯ }

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
⊢ Nonempty ↑C.pt.toTop

Tactic:
have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv

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)
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

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 g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
refine this.imp fun j hj => ?_

Result:
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

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
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
cases isEmpty_or_nonempty S

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)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

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)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

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
⊢ False

Tactic:
haveI : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h

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)
h : ∀ (x : J), Nonempty ↑(F.obj x).toTop
this : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
⊢ False

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
⊢ False

Tactic:
suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)

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)
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
⊢ Nonempty ↑C.pt.toTop

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)
⊢ False

Tactic:
haveI : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
  (inferInstance : T2Space (F.obj j))

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)
h : ∀ (x : J), Nonempty ↑(F.obj x).toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False