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)) α
intro :
  ∀ (val : Fintype α),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (α → Fin 2)),
      LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) 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))
      (α → Fin 2)),
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
cases nonempty_fintype α

Premises used: nonempty_fintype
-- 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
⊢ ∀ (a : α),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (Fin 2)),
      ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
have hff := fun a : α => exists_locallyConstant_fin_two _ hC (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
hff :
  ∀ (a : α),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (Fin 2)),
      ff a = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g
intro :
  ∀ (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)),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (α → Fin 2)),
      LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) 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))
      (α → Fin 2)),
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
choose j g h using hff
-- 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
intro :
  ∀ (j0 : J) (hj0 : ∀ {X : J}, X ∈ G → Nonempty.{v + 1} (j0 ⟶ X)),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (α → Fin 2)),
      LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) 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))
      (α → Fin 2)),
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
obtain ⟨j0, hj0⟩ := IsCofiltered.inf_objs_exists G

Premises used: CategoryTheory.IsCofiltered.inf_objs_exists
-- 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)
⊢ ∀ (a : α), j a ∈ Finset.image j Finset.univ

Tactic:
grind
-- 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)
⊢ ∀ (a : α), j a ∈ Finset.image j Finset.univ

Tactic:
have hj : ∀ a, j a ∈ (Finset.univ.image j : Finset J) := by grind
-- 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
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (α → Fin 2)),
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
⟨j0, ggg, ?_⟩

Premises used: Exists.intro
-- 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 :
  LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (α → Fin 2)),
    LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
      LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
refine ⟨j0, ggg, ?_⟩
-- 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
⊢ LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip

Tactic:
simp
-- 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
⊢ LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip

Tactic:
have : f.map ι = LocallyConstant.unflip (f.map ι).flip := by simp
-- 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
this : LocallyConstant.map ι f = LocallyConstant.unflip (LocallyConstant.map ι f).flip
intro :
  LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg
⊢ LocallyConstant.map (fun (a b : α) ↦ if a = b then 0 else 1) f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg

Tactic:
rw [this]
-- 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
⊢ LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip

Tactic:
simp
-- 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
⊢ LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip

Tactic:
have :
    LocallyConstant.comap (C.π.app j0).hom.hom ggg =
      LocallyConstant.unflip (LocallyConstant.comap (C.π.app j0).hom.hom ggg).flip := by
    simp
-- 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
this :
  LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
intro :
  LocallyConstant.unflip (LocallyConstant.map ι f).flip =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg

Tactic:
rw [this]
-- 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 : (LocallyConstant.map ι f).flip = (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip
⊢ LocallyConstant.unflip (LocallyConstant.map ι f).flip =
    LocallyConstant.unflip (LocallyConstant.comap (TopCat.Hom.hom (C.π.app j0).hom) ggg).flip

Tactic:
congr 1