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
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:
exact hj.elim' (C.π.app j x)

Premises used: CategoryTheory.Limits.Cone.π, CategoryTheory.ConcreteCategory.hom, IsEmpty.elim', DFunLike.coe, CategoryTheory.NatTrans.app
-- 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)
inl :
  ∃ (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:
suffices ∃ j, IsEmpty (F.obj j) by
      refine this.imp fun j hj => ?_
      refine ⟨⟨hj.elim, fun A => ?_⟩, ?_⟩
      · convert! isOpen_empty
        ext x
        exact hj.elim x
      · ext x
        exact hj.elim' (C.π.app j 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)
inl :
  ∀
    (h :
      ∀ (j : J),
        Nonempty
          (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
            Type (max u v))),
    False
⊢ ∃ (j : J),
    IsEmpty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))

Tactic:
by_contra! 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
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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))

Tactic:
haveI : ∀ j : J, Nonempty ((F ⋙ Profinite.toTopCat).obj j) := 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
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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
⊢ ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))

Tactic:
haveI : ∀ j : J, T2Space ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : T2Space (F.obj j))
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
⊢ ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))

Tactic:
haveI : ∀ j : J, CompactSpace ((F ⋙ Profinite.toTopCat).obj j) := fun j =>
      (inferInstance : CompactSpace (F.obj j))
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
⊢ Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))

Tactic:
have cond := TopCat.nonempty_limitCone_of_compact_t2_cofiltered_system.{u}
      (F ⋙ Profinite.toTopCat)
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
cond : Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))
inl : Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ False

Tactic:
suffices Nonempty C.pt from IsEmpty.false (S.proj this.some)
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
cond : Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
inl :
  ∀ (hD : IsLimit D),
    Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))

Tactic:
have hD : IsLimit D := isLimitOfPreserves Profinite.toTopCat hC
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
cond : Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
inl :
  ∀ (CD : (TopCat.limitCone (F ⋙ toTopCat)).pt ⟶ D.pt),
    Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))

Tactic:
have CD := (hD.conePointUniqueUpToIso (TopCat.limitConeIsLimit.{v, max u v} _)).inv
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
cond : Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
CD : (TopCat.limitCone (F ⋙ toTopCat)).pt ⟶ D.pt
⊢ Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))

Tactic:
cond.map CD

Premises used: CategoryTheory.ConcreteCategory.hom, Nonempty.map, DFunLike.coe
-- 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)
h :
  ∀ (j : J),
    Nonempty
      (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
this_1 : ∀ (j : J), Nonempty (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this_2 : ∀ (j : J), T2Space (↑((F ⋙ toTopCat).obj j) : Type (max u v))
this : ∀ (j : J), CompactSpace (↑((F ⋙ toTopCat).obj j) : Type (max u v))
cond : Nonempty (↑(TopCat.limitCone.{v, u, v} (F ⋙ toTopCat)).pt : Type (max v u))
D : Cone (F ⋙ toTopCat) := toTopCat.mapCone C
hD : IsLimit D
CD : (TopCat.limitCone (F ⋙ toTopCat)).pt ⟶ D.pt
⊢ Nonempty (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))

Tactic:
exact cond.map CD

Premises used: CategoryTheory.ConcreteCategory.hom, Nonempty.map, DFunLike.coe
-- 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 : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (Quotient S.toSetoid) :=
  { toFun := S.proj, isLocallyConstant := ⋯ }
inr :
  ∀ (j : J)
    (g' :
      LocallyConstant
        (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
        (Quotient S.toSetoid))
    (hj : 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
⊢ ∃ (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, g', hj⟩ := exists_locallyConstant_finite_nonempty _ hC f'

Premises used: Profinite.exists_locallyConstant_finite_nonempty
-- 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 : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (Quotient S.toSetoid) :=
  { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Quotient S.toSetoid)
hj : 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:
⟨j, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩

Premises used: LocallyConstant.mk, Function.comp, LocallyConstant.isLocallyConstant, Exists.intro, IsLocallyConstant.comp, DFunLike.coe
-- 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 : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (Quotient S.toSetoid) :=
  { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
inr :
  f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom)
      { toFun := ff ∘ (⇑g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid), isLocallyConstant := ⋯ }
⊢ ∃ (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, ⟨ff ∘ g', g'.isLocallyConstant.comp _⟩, ?_⟩
-- 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 : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (Quotient S.toSetoid) :=
  { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
inr :
  ∀ (t : (↑(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))) → α) t : α)
      ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom)
              { toFun := ff ∘ (⇑g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid),
                isLocallyConstant := ⋯ :
                LocallyConstant
                  (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) :
                    Type (max u v))
                  α } :
            (a : (↑C.pt.toTop : Type (max u v))) → α)
          t :
        α)
⊢ f =
    LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom)
      { toFun := ff ∘ (⇑g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid), isLocallyConstant := ⋯ }

Tactic:
ext1 t
-- 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 : Nonempty (Quotient S.toSetoid)
f' : LocallyConstant
  (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
  (Quotient S.toSetoid) :=
  { toFun := S.proj, isLocallyConstant := ⋯ }
j : J
g' :
  LocallyConstant
    (↑((F.obj j).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
    (Quotient S.toSetoid)
hj : f' = LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g'
t : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
⊢ Eq (α := Quotient S.toSetoid)
    ((f' : (a : (↑C.pt.toTop : Type (max u v))) → Quotient S.toSetoid) t : Quotient S.toSetoid)
    ((LocallyConstant.comap (TopCat.Hom.hom (C.π.app j).hom) g' :
          (a : (↑C.pt.toTop : Type (max u v))) → Quotient S.toSetoid)
        t :
      Quotient S.toSetoid)

Tactic:
apply_fun fun e => e t at hj