awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X Y : Profinite
f : X ⟶ Y
mpr :
  Epi (X :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        X)
      (Y :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Y)
      (↾(⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              Y)) →
    Epi f
⊢ Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Y)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u)) Y) →
    Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]

Premises used: CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.Topology.Category.Profinite.Basic
Goal:
X Y : Profinite
f : X ⟶ Y
⊢ Epi (X :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        X)
      (Y :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u))
        Y)
      (↾(⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)) f) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
              Y)) →
    Epi f

Tactic:
apply (forget Profinite).epi_of_epi_map

Premises used: Profinite, CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
i : J
refine_1 :
  TopologicalSpace.IsTopologicalBasis (α :=
    (↑((F.obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    {W :
      Set
        (↑((F.obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) |
      IsClopen W}
⊢ TopologicalSpace.IsTopologicalBasis (α := (↑((F ⋙ toTopCat).obj i) : Type (max u v)))
    ((fun (j : J) ↦
        ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
          Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
      i)

Tactic:
change TopologicalSpace.IsTopologicalBasis {W : Set (F.obj i) | IsClopen W}

Premises used: setOf, TopologicalSpace.IsTopologicalBasis, IsClopen
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
i : J
⊢ TopologicalSpace.IsTopologicalBasis (α :=
    (↑((F.obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    {W :
      Set
        (↑((F.obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) |
      IsClopen W}

Tactic:
apply isTopologicalBasis_isClopen

Premises used: isTopologicalBasis_isClopen
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))
hV : IsClopen V
⊢ Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj i) : Type (max u v))))
    ((fun (j : J) ↦
        ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
          Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
      i)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            TopCat.carrier) ((F ⋙ toTopCat).map f)) :
        (a : (↑((F ⋙ toTopCat).obj i) : Type (max u v))) → (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
      V)

Tactic:
⟨hV.1.preimage ?_, hV.2.preimage ?_⟩

Premises used: Set.Mem, setOf, And.right, And.left, And.intro, IsClosed.preimage, IsClopen, IsOpen.preimage
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))
hV : IsClopen V
refine_2 refine_2₁ :
  Continuous (X := (↑((F ⋙ toTopCat).obj i) : Type (max u v))) (Y := (↑((F ⋙ toTopCat).obj j) : Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
          TopCat.carrier) ((F ⋙ toTopCat).map f)) :
      (a : (↑((F ⋙ toTopCat).obj i) : Type (max u v))) → (↑((F ⋙ toTopCat).obj j) : Type (max u v)))
⊢ Membership.mem (γ := Set (Set (↑((F ⋙ toTopCat).obj i) : Type (max u v))))
    ((fun (j : J) ↦
        ({W : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)) | IsClopen W} :
          Set (Set (↑((F ⋙ toTopCat).obj j) : Type (max u v)))))
      i)
    ((⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
            TopCat.carrier) ((F ⋙ toTopCat).map f)) :
        (a : (↑((F ⋙ toTopCat).obj i) : Type (max u v))) → (↑((F ⋙ toTopCat).obj j) : Type (max u v))) ⁻¹'
      V)

Tactic:
refine ⟨hV.1.preimage ?_, hV.2.preimage ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hC : IsLimit C
hU : IsClopen U
i j : J
f : i ⟶ j
V : Set (↑((F ⋙ toTopCat).obj j) : Type (max u v))
hV : IsClopen V
⊢ Continuous (X := (↑((F ⋙ toTopCat).obj i) : Type (max u v))) (Y := (↑((F ⋙ toTopCat).obj j) : Type (max u v)))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat) ↦ C((↑X : Type (max u v)), (↑Y : Type (max u v)))) (CC :=
          TopCat.carrier) ((F ⋙ toTopCat).map f)) :
      (a : (↑((F ⋙ toTopCat).obj i) : Type (max u v))) → (↑((F ⋙ toTopCat).obj j) : Type (max u v)))

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
⊢ IsClopen U

Tactic:
have hU : IsClopen U := f.isLocallyConstant.isClopen_fiber _
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
obtain :
  ∀ (j : J)
    (V :
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (hV : IsClopen V)
    (h :
      U =
        (⇑(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)) ⁻¹'
          V),
    ∃ (j : J) (g :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (Fin 2)),
      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)),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

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

Premises used: Profinite.exists_isClopen_of_cofiltered
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(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)) ⁻¹'
      V
h₁ : f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)
⊢ ∃ (j : J) (g :
    LocallyConstant
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
      (Fin 2)),
    f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g

Tactic:
use j, LocallyConstant.ofIsClopen hV

Premises used: LocallyConstant.ofIsClopen
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(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)) ⁻¹'
      V
h₁ :
  Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    (Set.preimage (β := Fin 2)
      (⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)) :
        (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
      {0})
⊢ f = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)

Tactic:
apply LocallyConstant.locallyConstant_eq_of_fiber_zero_eq

Premises used: LocallyConstant.locallyConstant_eq_of_fiber_zero_eq
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(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)) ⁻¹'
      V
h₁ :
  Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    ((⇑(TopCat.Hom.hom (C.π.app j).hom) :
        (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) ⁻¹'
      V)
⊢ Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    (Set.preimage (β := Fin 2)
      (⇑(LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) (LocallyConstant.ofIsClopen (U := V) hV)) :
        (a : (↑C.pt.toTop : Type (max u v))) → Fin 2)
      {0})

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

Premises used: LocallyConstant.ofIsClopen_fiber_zero, LocallyConstant.coe_comap, Set.preimage_comp, Fin.isValue, 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(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)) ⁻¹'
      V
⊢ Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    ((⇑(TopCat.Hom.hom (C.π.app j).hom) :
        (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) ⁻¹'
      V)

Tactic:
h
-- Module: Mathlib.Topology.Category.Profinite.CofilteredLimit
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsCofiltered J
F : J ⥤ Profinite
C : Cone F
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) (Fin 2)
U : Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0}
hU : IsClopen U
j : J
V : Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hV : IsClopen V
h :
  U =
    (⇑(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)) ⁻¹'
      V
⊢ Eq (α :=
    Set (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    (Set.preimage (β := Fin 2) (⇑f : (a : (↑C.pt.toTop : Type (max u v))) → Fin 2) {0})
    ((⇑(TopCat.Hom.hom (C.π.app j).hom) :
        (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) ⁻¹'
      V)

Tactic:
exact h