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 α
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))
⊢ ι ((f : (a : (↑C.pt.toTop : Type (max u v))) → α) x) =
    (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))

Tactic:
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]
    rfl
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
inl :
  IsEmpty (Quotient S.toSetoid) →
    ∃ (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
inr :
  Nonempty (Quotient S.toSetoid) →
    ∃ (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:
cases isEmpty_or_nonempty S

Premises used: DiscreteQuotient.toSetoid, isEmpty_or_nonempty, Quotient
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ ∃ (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:
this.imp fun j hj => ?_

Premises used: Exists.imp
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
refine :
  ∀ (j : J)
    (hj :
      IsEmpty
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
    ∃ (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:
refine this.imp fun j hj => ?_

Premises used: Exists.imp
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ ∃ (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:
⟨⟨hj.elim, fun A => ?_⟩, ?_⟩

Premises used: LocallyConstant.mk, IsEmpty.elim, 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
refine_1 :
  ∀ (A : Set α),
    IsOpen (X :=
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ((fun
            (a :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          hj.elim (p :=
            fun
              (x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            α) a) ⁻¹'
        A)
refine_2 :
  f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom)
      {
        toFun :=
          fun
            (a :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          hj.elim (p :=
            fun
              (x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            α) a,
        isLocallyConstant := ⋯ }
⊢ ∃ (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 ⟨⟨hj.elim, fun 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
A : Set α
⊢ IsOpen (X :=
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))) ∅

Tactic:
isOpen_empty

Premises used: isOpen_empty
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h_1 : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
A : Set α
h :
  Eq (α :=
    Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    ((fun
          (a :
            (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v))) ↦
        hj.elim (p :=
          fun
            (x :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          α) a) ⁻¹'
      A)
    ∅
⊢ IsOpen (X :=
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    ((fun
          (a :
            (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v))) ↦
        hj.elim (p :=
          fun
            (x :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          α) a) ⁻¹'
      A)

Tactic:
convert! isOpen_empty

Premises used: isOpen_empty
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h_1 : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
A : Set α
h :
  ∀
    (x :
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))),
    Membership.mem (γ :=
        Set
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v)))
        ((fun
              (a :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            hj.elim (p :=
              fun
                (x :
                  (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))) ↦
              α) a) ⁻¹'
          A)
        x ↔
      Membership.mem (γ :=
        Set
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v)))
        ∅ x
⊢ Eq (α :=
    Set (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
    ((fun
          (a :
            (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
              Type (max u v))) ↦
        hj.elim (p :=
          fun
            (x :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          α) a) ⁻¹'
      A)
    ∅

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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
A : Set α
x : (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Membership.mem (γ :=
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ((fun
            (a :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          hj.elim (p :=
            fun
              (x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            α) a) ⁻¹'
        A)
      x ↔
    Membership.mem (γ :=
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ∅ x

Tactic:
hj.elim x

Premises used: IsEmpty.elim
-- 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
A : Set α
x : (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Membership.mem (γ :=
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ((fun
            (a :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          hj.elim (p :=
            fun
              (x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            α) a) ⁻¹'
        A)
      x ↔
    Membership.mem (γ :=
      Set
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)))
      ∅ x

Tactic:
exact hj.elim 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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
refine_2 :
  ∀ (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)
              {
                toFun :=
                  fun
                    (a :
                      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))) ↦
                  hj.elim (p :=
                    fun
                      (x :
                        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                          Type (max u v))) ↦
                    α) a,
                isLocallyConstant := ⋯ } :
            (a : (↑C.pt.toTop : Type (max u v))) → α)
          x :
        α)
⊢ f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom)
      {
        toFun :=
          fun
            (a :
              (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                Type (max u v))) ↦
          hj.elim (p :=
            fun
              (x :
                (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                  Type (max u v))) ↦
            α) a,
        isLocallyConstant := ⋯ }

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
hC : IsLimit C
f :
  LocallyConstant
    (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) α
S : DiscreteQuotient
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v)) :=
  f.discreteQuotient
ff : Quotient S.toSetoid → α := (⇑f.lift : (a : Quotient f.discreteQuotient.toSetoid) → α)
h : IsEmpty (Quotient S.toSetoid)
this :
  ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
j : J
hj :
  IsEmpty (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
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)
            {
              toFun :=
                fun
                  (a :
                    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                      Type (max u v))) ↦
                hj.elim (p :=
                  fun
                    (x :
                      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                        Type (max u v))) ↦
                  α) a,
              isLocallyConstant := ⋯ } :
          (a : (↑C.pt.toTop : Type (max u v))) → α)
        x :
      α)

Tactic:
hj.elim' (C.π.app j x)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, IsEmpty.elim', DFunLike.coe, CategoryTheory.NatTrans.app