J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let S := f.discreteQuotient
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let ff : S → α := f.lift
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g

case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
cases isEmpty_or_nonempty S
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ¬∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
simp only [← not_nonempty_iff, ← not_forall]
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
⊢ False
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
⊢ ¬∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
intro h
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
⊢ False
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
⊢ False
haveI : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := h
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
⊢ False
haveI : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
  (inferInstance : T2Space (F.obj j))
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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)
⊢ False
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.toTop
this✝ : ∀ (j : J), Nonempty ↑((F ⋙ toTopCat).obj j)
this : ∀ (j : J), T2Space ↑((F ⋙ toTopCat).obj j)
⊢ False
haveI : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
  (inferInstance : CompactSpace (F.obj j))
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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)
⊢ False
have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u, u}
  (F ⋙ Profinite.toTopCat)
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
this : Nonempty ↑C.pt.toCompHaus.toTop
⊢ False

case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
suffices : Nonempty C.pt
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
case inl
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
this : Nonempty ↑C.pt.toCompHaus.toTop
⊢ False

case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
exact IsEmpty.false (S.proj this.some)
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
⊢ Nonempty ↑C.pt.toCompHaus.toTop
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
let D := Profinite.toTopCat.mapCone C
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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
⊢ Nonempty ↑C.pt.toCompHaus.toTop
have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{u, u} _)).inv
no goals
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
h : ∀ (x : J), Nonempty ↑(F.obj x).toCompHaus.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.toCompHaus.toTop
exact cond.map CD
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ ∃ g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
refine' this.imp fun j hj => _
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)

case refine'_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j))
      { toFun := fun a => IsEmpty.elim hj a,
        isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) }
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ ∃ g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
refine' ⟨⟨hj.elim, fun A => _⟩, _⟩
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)

case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)
suffices : (fun a ↦ IsEmpty.elim hj a) ⁻¹' A = ∅
no goals
case this
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
⊢ (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
exact @Set.eq_empty_of_isEmpty _ hj _
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ∅
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)
rw [this]
no goals
case refine'_1
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this✝ : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
A : Set α
this : (fun a => IsEmpty.elim hj a) ⁻¹' A = ∅
⊢ IsOpen ∅
exact isOpen_empty
case refine'_2.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := fun a => IsEmpty.elim hj a,
            isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) })
      x
case refine'_2
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
⊢ f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j))
      { toFun := fun a => IsEmpty.elim hj a,
        isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) }
ext x
no goals
case refine'_2.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : IsEmpty (Quotient S.toSetoid)
this : ∃ j, IsEmpty ↑(F.obj j).toCompHaus.toTop
j : J
hj : IsEmpty ↑(F.obj j).toCompHaus.toTop
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := fun a => IsEmpty.elim hj a,
            isLocallyConstant := (_ : ∀ (A : Set α), IsOpen ((fun a => IsEmpty.elim hj a) ⁻¹' A)) })
      x
exact hj.elim' (C.π.app j x)
case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let f' : LocallyConstant C.pt S := ⟨S.proj, S.proj_isLocallyConstant⟩
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case inr
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
obtain ⟨j, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
⊢ f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j))
      { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) }
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
refine' ⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, _⟩
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
t : ↑C.pt.toCompHaus.toTop
⊢ ↑f t =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
case inr.intro.intro
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
⊢ f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j))
      { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) }
ext1 t
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g') t
⊢ ↑f t =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g'
t : ↑C.pt.toCompHaus.toTop
⊢ ↑f t =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
apply_fun fun e => e t at hj
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = (↑g' ∘ (forget Profinite).map (C.π.1 j)) t
⊢ ↑f t =
    (↑{ toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) } ∘
        (forget Profinite).map (C.π.1 j))
      t
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g') t
⊢ ↑f t =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j))
          { toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) })
      t
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j).continuous] at hj ⊢
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' ((forget Profinite).map (C.π.1 j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (↑g' ((forget Profinite).map (C.π.1 j) t))
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : ↑f' t = (↑g' ∘ (forget Profinite).map (C.π.1 j)) t
⊢ ↑f t =
    (↑{ toFun := ff ∘ ↑g', isLocallyConstant := (_ : IsLocallyConstant (ff ∘ g'.toFun)) } ∘
        (forget Profinite).map (C.π.1 j))
      t
dsimp at hj ⊢
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' ((forget Profinite).map (C.π.1 j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t)
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' ((forget Profinite).map (C.π.1 j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (↑g' ((forget Profinite).map (C.π.1 j) t))
rw [← hj]
no goals
case inr.intro.intro.h
J : Type u
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
S : DiscreteQuotient ↑C.pt.toCompHaus.toTop := LocallyConstant.discreteQuotient f
ff : Quotient S.toSetoid → α := ↑(LocallyConstant.lift f)
h✝ : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant (↑C.pt.toCompHaus.toTop) (Quotient S.toSetoid) :=
  { toFun := DiscreteQuotient.proj S, isLocallyConstant := (_ : IsLocallyConstant (DiscreteQuotient.proj S)) }
j : J
g' : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (Quotient S.toSetoid)
t : ↑C.pt.toCompHaus.toTop
hj : DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t = ↑g' ((forget Profinite).map (C.π.1 j) t)
⊢ ↑f t = ↑(LocallyConstant.lift f) (DiscreteQuotient.proj (LocallyConstant.discreteQuotient f) t)
rfl