-- Mathlib/Topology/Category/Profinite/CofilteredLimit.lean
theorem exists_locallyConstant_fin_two (hC : IsLimit C) (f : LocallyConstant C.pt (Fin 2)) :
    ∃ (j : J) (g : LocallyConstant (F.obj j) (Fin 2)), f = g.comap (C.π.app _).hom

Proof state:
case h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) (LocallyConstant.ofIsClopen hV)) ⁻¹' {0}

Tactic:
simp only [Fin.isValue, Functor.const_obj_obj, LocallyConstant.coe_comap, Set.preimage_comp,
  LocallyConstant.ofIsClopen_fiber_zero]

Result:
case h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(TopCat.Hom.hom (C.π.app j)) ⁻¹' V

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
obtain ⟨j, V, hV, h⟩ := exists_isClopen_of_cofiltered C hC hU

Result:
case intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Proof state:
case intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
classical
use j, LocallyConstant.ofIsClopen hV
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
simp only [Fin.isValue, Functor.const_obj_obj, LocallyConstant.coe_comap, Set.preimage_comp,
  LocallyConstant.ofIsClopen_fiber_zero]
erw [← h]

Result:
no goals

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
let U := f ⁻¹' {0}

Result:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Proof state:
case intro.intro.intro
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
use j, LocallyConstant.ofIsClopen hV

Result:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) (LocallyConstant.ofIsClopen hV)

Proof state:
case h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(TopCat.Hom.hom (C.π.app j)) ⁻¹' V

Tactic:
erw [← h]

Result:
no goals

Proof state:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Tactic:
have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _

Result:
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
⊢ ∃ j g, f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) g

Proof state:
case h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) (LocallyConstant.ofIsClopen hV)

Tactic:
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq

Result:
case h.h
J : Type v
inst✝¹ : SmallCategory J
inst✝ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f : LocallyConstant (↑C.pt.toTop) (Fin 2)
U : Set ↑C.pt.toTop := ⇑f ⁻¹' {0}
hU : IsClopen U
j : J
V : Set ↑(F.obj j).toTop
hV : IsClopen V
h : U = ⇑(ConcreteCategory.hom (C.π.app j)) ⁻¹' V
⊢ ⇑f ⁻¹' {0} = ⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j)) (LocallyConstant.ofIsClopen hV)) ⁻¹' {0}