awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
intro :
  ∀ (a : α), (LocallyConstant.map ι f).flip a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
⊢ (LocallyConstant.map ι f).flip = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip

Tactic:
ext1 a
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
intro : ff a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
⊢ (LocallyConstant.map ι f).flip a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a

Tactic:
change ff a = _
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
intro :
  LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
    (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
⊢ ff a = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a

Tactic:
rw [h]
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
intro :
  LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
    (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a
⊢ LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
    (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a

Tactic:
dsimp
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
val : Fintype α
ι : α → α → Fin 2 := fun (x y : α) ↦ if x = y then 0 else 1
ff : (a : α) →
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2) :=
  (LocallyConstant.map ι f).flip
j : (a : α) → J
g :
  (a : α) →
    LocallyConstant
      (↑((F.obj (j a)).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)
h : ∀ (a : α), ff a = LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a)
G : Finset J := Finset.image j Finset.univ
j0 : J
hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)
hj : ∀ (a : α), j a ∈ Finset.image j Finset.univ
fs : (a : α) → j0 ⟶ j a := fun (a : α) ↦ ⋯.some
gg : α →
  LocallyConstant
    (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Fin 2) :=
  fun (a : α) ↦ LocallyConstant.comap (TopCat.Hom.hom (F.map (fs a)).hom) (g a)
ggg : LocallyConstant
  (↑((F.obj j0).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (α → Fin 2) :=
  LocallyConstant.unflip gg
a : α
intro :
  ∀ (x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
    Eq (α := Fin 2)
      ((LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) :
            (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
          x :
        Fin 2)
      (((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a :
            (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
          x :
        Fin 2)
⊢ LocallyConstant.comap (TopCat.Hom.hom (InducedCategory.Hom.hom (C.π.app (j a)))) (g a) =
    (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip a

Tactic:
ext1 x
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabit :
  ∀ (inhabited_h : Inhabited α),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        α),
      f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
inhabit α
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
obtain :
  ∀ (j : J)
    (gg :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (α → Fin 2))
    (h :
      LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
        LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        α),
      f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
obtain ⟨j, gg, h⟩ := exists_locallyConstant_finite_aux _ hC f

Premises used: Profinite.exists_locallyConstant_finite_aux
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
⟨j, gg.map σ, ?_⟩

Premises used: Exists.intro, LocallyConstant.map
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
refine : f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg)
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
refine ⟨j, gg.map σ, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
h₁ :
  ∀ (x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
    Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
      ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg) :
            (a : (↑C.pt.toTop : Type (max u v))) → α)
          x :
        α)
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg)

Tactic:
ext x
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
h₁ :
  (f : (a : (↑C.pt.toTop : Type (max u v))) → α) x =
    σ
      ((gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
        ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
            x :
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v))))
⊢ Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
    ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.map σ gg) :
          (a : (↑C.pt.toTop : Type (max u v))) → α)
        x :
      α)

Tactic:
simp only [Functor.const_obj_obj, LocallyConstant.coe_comap, LocallyConstant.map_apply,
    Function.comp_apply]

Premises used: LocallyConstant.map_apply, LocallyConstant.coe_comap, Function.comp_apply, CategoryTheory.Functor.const_obj_obj
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
h₁ :
  Eq.{u_1 + 1} (α := α) ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x : α)
    (if h :
          ∃ (a : α),
            ι a =
              (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
                ((TopCat.Hom.hom (C.π.app j).hom :
                      (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
                    x :
                  (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))) then
        h.choose (p := fun (a : α) ↦
          ι a =
            (gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
              ((TopCat.Hom.hom (C.π.app j).hom :
                    (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
                  x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))))
      else default :
      α)
⊢ (f : (a : (↑C.pt.toTop : Type (max u v))) → α) x =
    σ
      ((gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
        ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
            x :
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v))))

Tactic:
dsimp [σ]
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
α : Type u_1
inst_2 : Finite α
inst_3 : Nonempty α
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
inhabited_h : Inhabited α
j : J
gg :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (α → Fin 2)
h :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg
ι : α → α → Fin 2 := fun (a b : α) ↦ if a = b then 0 else 1
σ : (α → Fin 2) → α :=
  fun (f : α → Fin 2) ↦ if h : ∃ (a : α), ι a = f then h.choose (p := fun (a : α) ↦ ι a = f) else default
x : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Eq.{u_1 + 1} (α := (b : α) → Fin 2)
    ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) gg :
          (a : (↑C.pt.toTop : Type (max u v))) → (b : α) → Fin 2)
        x :
      (b : α) → Fin 2)
    ((gg : (a : (↑(F.obj j).toTop : Type (max u v))) → α → Fin 2)
        ((ConcreteCategory.hom (FC :=
                fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v)),
                  (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))))
                (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
                (C.π.app j) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                      (↑X.toTop : Type (max u v)))
                    (((Functor.const J).obj C.pt).obj j)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
                    (↑X.toTop : Type (max u v)))
                  (F.obj j))
            x :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v))) ↦
              (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
            (F.obj j)) :
      α → Fin 2)

Tactic:
rfl