J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
⊢ ∃ 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
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
inhabit α
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
⊢ ∃ 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
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
⊢ ∃ j g, 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 α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ ∃ j g, 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 α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
let σ : (α → Fin 2) → α := fun f => if h : ∃ a : α, ι a = f then h.choose else default
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.map σ gg)
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ ∃ j g, f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) g
refine' ⟨j, gg.map σ, _⟩
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.map σ gg)) x
case intro.intro
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
⊢ f = LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.map σ gg)
ext x
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = (↑(LocallyConstant.map σ gg) ∘ (forget Profinite).map (C.π.1 j)) x
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = ↑(LocallyConstant.comap ((forget Profinite).map (C.π.app j)) (LocallyConstant.map σ gg)) x
rw [LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j).continuous]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x = (↑(LocallyConstant.map σ gg) ∘ (forget Profinite).map (C.π.1 j)) x
dsimp
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
have h1 : ι (f x) = gg (C.π.app j x) := by
  change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
  rw [h, LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j).continuous]
  rfl
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
have h2 : ∃ a : α, ι a = gg (C.π.app j x) := ⟨f x, h1⟩
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x = Exists.choose h2
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x =
    if h : ∃ a, (fun b => if a = b then 0 else 1) = ↑gg ((forget Profinite).map (C.π.1 j) x) then Exists.choose h
    else default
rw [dif_pos h2]
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ι (↑f x) = ι (Exists.choose h2)

case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ Function.Injective ι
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ↑f x = Exists.choose h2
apply_fun ι
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑(LocallyConstant.map (fun a b => if a = b then 0 else 1) f) x = ↑gg ((forget Profinite).map (C.π.app j) x)
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
change f.map (fun a b => if a = b then (0 : Fin 2) else 1) x = _
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ (↑gg ∘ (forget Profinite).map (C.π.1 j)) x = ↑gg ((forget Profinite).map (C.π.app j) x)
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ ↑(LocallyConstant.map (fun a b => if a = b then 0 else 1) f) x = ↑gg ((forget Profinite).map (C.π.app j) x)
rw [h, LocallyConstant.coe_comap ((forget Profinite).map _) _ (C.π.app j).continuous]
no goals
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
⊢ (↑gg ∘ (forget Profinite).map (C.π.1 j)) x = ↑gg ((forget Profinite).map (C.π.app j) x)
rfl
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ι (↑f x) = ι (Exists.choose h2)
rw [h2.choose_spec]
no goals
case intro.intro.h
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
exact h1
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
⊢ a = b
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
⊢ Function.Injective ι
intro a b hh
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : ι a a = ι b a
⊢ a = b
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
⊢ a = b
have hhh := congr_fun hh a
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : (if a = a then 0 else 1) = if b = a then 0 else 1
⊢ a = b
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : ι a a = ι b a
⊢ a = b
dsimp at hhh
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : 0 = if b = a then 0 else 1
⊢ a = b
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : (if a = a then 0 else 1) = if b = a then 0 else 1
⊢ a = b
rw [if_pos rfl] at hhh
case intro.intro.h.inj.inl
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hh1 : b = a
hhh : 0 = 0
⊢ a = b

case intro.intro.h.inj.inr
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hh1 : ¬b = a
hhh : 0 = 1
⊢ a = b
case intro.intro.h.inj
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hhh : 0 = if b = a then 0 else 1
⊢ a = b
split_ifs at hhh with hh1
no goals
case intro.intro.h.inj.inl
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hh1 : b = a
hhh : 0 = 0
⊢ a = b
exact hh1.symm
no goals
case intro.intro.h.inj.inr
J : Type u
inst✝³ : SmallCategory J
inst✝² : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst✝¹ : Finite α
inst✝ : Nonempty α
hC : IsLimit C
f : LocallyConstant (↑C.pt.toCompHaus.toTop) α
inhabited_h : Inhabited α
j : J
gg : LocallyConstant (↑(F.obj j).toCompHaus.toTop) (α → Fin 2)
h :
  LocallyConstant.map (fun a b => if a = b then 0 else 1) f =
    LocallyConstant.comap ((forget Profinite).map (C.π.app j)) gg
ι : α → α → Fin 2 := fun a b => if a = b then 0 else 1
σ : (α → Fin 2) → α := fun f => if h : ∃ a, ι a = f then Exists.choose h else default
x : ↑C.pt.toCompHaus.toTop
h1 : ι (↑f x) = ↑gg ((forget Profinite).map (C.π.app j) x)
h2 : ∃ a, ι a = ↑gg ((forget Profinite).map (C.π.app j) x)
a b : α
hh : ι a = ι b
hh1 : ¬b = a
hhh : 0 = 1
⊢ a = b
exact False.elim (bot_ne_top hhh)