case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) 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
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
cases nonempty_fintype α
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let ff := (f.map ι).flip
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
have hff := fun a : α => exists_locallyConstant_fin_two _ hC (ff a)
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
hff : ∀ (a : α), ∃ j g, ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
choose j g h using hff
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let G : Finset J := Finset.univ.image j
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists G
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
have hj : ∀ a, j a ∈ (Finset.univ.image j : Finset J) := by
  intro a
  simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let fs : ∀ a : α, j0 ⟶ j a := fun a => (hj0 (hj a)).some
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let gg : α → LocallyConstant (F.obj j0) (Fin 2) := fun a => (g a).comap (F.map (fs _))
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let ggg := LocallyConstant.unflip gg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ ∃ j g,
    LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
      LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
refine' ⟨j0, ggg, _⟩
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
have : f.map ι = LocallyConstant.unflip (f.map ι).flip := by simp
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
rw [this]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
clear this
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
have :
  LocallyConstant.comap (C.π.app j0) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0) ggg).flip :=
  by simp
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg
rw [this]
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
this :
  LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
clear this
case intro.intro.e_f
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.flip (LocallyConstant.map ι f) =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg)
case intro.intro
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f)) =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
congr 1
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.flip (LocallyConstant.map ι f) a =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
case intro.intro.e_f
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.flip (LocallyConstant.map ι f) =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg)
ext1 a
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ ff a = LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.flip (LocallyConstant.map ι f) a =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
change ff a = _
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a) =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ ff a = LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
rw [h]
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a) =
    LocallyConstant.flip
      (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
        (LocallyConstant.unflip fun a =>
          LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
      a
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a) =
    LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg) a
dsimp
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
case intro.intro.e_f.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
⊢ LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a) =
    LocallyConstant.flip
      (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
        (LocallyConstant.unflip fun a =>
          LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
      a
ext1 x
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (↑(g a) ∘ (forget Profinite).map (C.π.1 (j a))) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app (j a)).continuous]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
          {
            toFun := fun x a =>
              ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
                x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
                        (g a))
                    x) })
      x a
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (↑(g a) ∘ (forget Profinite).map (C.π.1 (j a))) x =
    ↑(LocallyConstant.flip
          (LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
            (LocallyConstant.unflip fun a =>
              LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a)))
          a)
      x
dsimp [LocallyConstant.flip, LocallyConstant.unflip]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    (↑{
            toFun := fun x a =>
              ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
                x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
                        (g a))
                    x) } ∘
        (forget Profinite).map (C.π.1 j0))
      x a
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j0))
          {
            toFun := fun x a =>
              ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
                x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
                        (g a))
                    x) })
      x a
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j0).continuous]
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
      ((forget Profinite).map (C.π.1 j0) x)
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    (↑{
            toFun := fun x a =>
              ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
                x,
            isLocallyConstant :=
              (_ :
                IsLocallyConstant fun x a =>
                  ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
                        (g a))
                    x) } ∘
        (forget Profinite).map (C.π.1 j0))
      x a
dsimp
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    (↑(g a) ∘ (forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
      ((forget Profinite).map (C.π.1 j0) x)

J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ Continuous ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(LocallyConstant.comap ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a))))) (g a))
      ((forget Profinite).map (C.π.1 j0) x)
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ _]
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
a : α
⊢ j a ∈ Finset.image j Finset.univ
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
⊢ ∀ (a : α), j a ∈ Finset.image j Finset.univ
intro a
no goals
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
a : α
⊢ j a ∈ Finset.image j Finset.univ
simp only [Finset.mem_image, Finset.mem_univ, true_and, exists_apply_eq_apply]
no goals
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.map ι f))
simp
no goals
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
⊢ LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg =
    LocallyConstant.unflip (LocallyConstant.flip (LocallyConstant.comap ((forget Profinite).map (C.π.app j0)) ggg))
simp
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(g a)
      ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) ((forget Profinite).map (C.π.1 j0) x))
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    (↑(g a) ∘ (forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
      ((forget Profinite).map (C.π.1 j0) x)
dsimp
case intro.intro.e_f.h.h.h.e'_6
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (forget Profinite).map (C.π.1 (j a)) x =
    (forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) ((forget Profinite).map (C.π.1 j0) x)
case intro.intro.e_f.h.h
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ ↑(g a) ((forget Profinite).map (C.π.1 (j a)) x) =
    ↑(g a)
      ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) ((forget Profinite).map (C.π.1 j0) x))
congr! 1
case intro.intro.e_f.h.h.h.e'_6
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (forget Profinite).map (C.π.1 (j a)) x = (forget Profinite).map (C.π.app j0 ≫ F.map (fs a)) x
case intro.intro.e_f.h.h.h.e'_6
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (forget Profinite).map (C.π.1 (j a)) x =
    (forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))) ((forget Profinite).map (C.π.1 j0) x)
change _ = (C.π.app j0 ≫ F.map (fs a)) x
no goals
case intro.intro.e_f.h.h.h.e'_6
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ (forget Profinite).map (C.π.1 (j a)) x = (forget Profinite).map (C.π.app j0 ≫ F.map (fs a)) x
rw [C.w]
no goals
J : Type u
inst✝² : SmallCategory J
inst✝¹ : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝ : Finite α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
val✝ : Fintype α
ι : α → α → Fin 2 := fun x y => if x = y then 0 else 1
ff : α → LocallyConstant (↑C.pt.toCompHaus.toTop) (Fin 2) := LocallyConstant.flip (LocallyConstant.map ι f)
j : α → J
g : (a : α) → LocallyConstant (↑(F.obj (j a)).toCompHaus.toTop) (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap ((forget Profinite).map (C.π.app (j a))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun a => Nonempty.some (_ : Nonempty (j0 ⟶ j a))
gg : α → LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (Fin 2) :=
  fun a => LocallyConstant.comap ((forget Profinite).map (F.map (fs a))) (g a)
ggg : LocallyConstant (↑(F.obj j0).toCompHaus.toTop) (α → Fin 2) := LocallyConstant.unflip gg
a : α
x : (forget Profinite).obj C.pt
⊢ Continuous ((forget Profinite).map (F.map (Nonempty.some (_ : Nonempty (j0 ⟶ j a)))))
exact (F.map _).continuous