-- Mathlib/Topology/Category/Profinite/Extend.lean
/--
A continuous map from a profinite set to a finite set factors through one of the components of
the profinite set when written as a cofiltered limit of finite sets.
-/
lemma exists_hom (hc : IsLimit c) {X : FintypeCat} (f : c.pt ⟶ toProfinite.obj X) :
    ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g

Proof state:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
let f' : LocallyConstant c.pt (toProfinite.obj X) :=
  ⟨f, (IsLocallyConstant.iff_continuous _).mpr f.hom.continuous⟩

Result:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Proof state:
case intro.intro
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
refine ⟨i, (g : _ → _), ?_⟩

Result:
case intro.intro
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
⊢ f = c.π.app i ≫ toProfinite.map ⇑g

Proof state:
case intro.intro.h.h
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
x : ↑c.pt.toTop
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.π.app i ≫ toProfinite.map ⇑g)) x

Tactic:
exact LocallyConstant.congr_fun h x

Result:
no goals

Proof state:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
let _ : TopologicalSpace X := ⊥

Result:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Proof state:
case intro.intro
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
⊢ f = c.π.app i ≫ toProfinite.map ⇑g

Tactic:
ext x

Result:
case intro.intro.h.h
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
x : ↑c.pt.toTop
⊢ (ConcreteCategory.hom f) x = (ConcreteCategory.hom (c.π.app i ≫ toProfinite.map ⇑g)) x

Proof state:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
obtain ⟨i, g, h⟩ := exists_locallyConstant.{_, u} c hc f'

Result:
case intro.intro
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
f' : LocallyConstant ↑c.pt.toTop ↑(toProfinite.obj X).toTop :=
  { toFun := ⇑(ConcreteCategory.hom f), isLocallyConstant := ⋯ }
i : I
g : LocallyConstant ↑((F ⋙ toProfinite).obj i).toTop ↑(toProfinite.obj X).toTop
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i)) g
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Proof state:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g

Tactic:
have : DiscreteTopology (toProfinite.obj X) := ⟨rfl⟩

Result:
I : Type u
inst✝¹ : SmallCategory I
inst✝ : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x✝ : TopologicalSpace X.carrier := ⊥
this : DiscreteTopology ↑(toProfinite.obj X).toTop
⊢ ∃ i g, f = c.π.app i ≫ toProfinite.map g