awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
⊢ Epi (X := ∐ X) (Sigma.desc π)

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
⊢ ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
⊢ ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      (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)) (π a) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (X a)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                B)
          x =
        b

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ EffectiveEpiFamily X π

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x :
        (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        (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)) (π a) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
3 ↔ 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
erw :
  (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := profiniteToCompHaus.obj B)
      (fun (a : α) ↦ profiniteToCompHaus.obj (X a)) fun (a : α) ↦ profiniteToCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x :
        (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        (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)) (π a) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)]

Premises used: profiniteToCompHaus, CategoryTheory.Functor.map, List.TFAE.out, OfNat.ofNat, CompHaus.effectiveEpiFamily_tfae, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := profiniteToCompHaus.obj B)
      (fun (a : α) ↦ profiniteToCompHaus.obj (X a)) fun (a : α) ↦ profiniteToCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π

Tactic:
⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩

Premises used: CategoryTheory.Functor.finite_effectiveEpiFamily_of_map, profiniteToCompHaus, inferInstance, Iff.intro
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (EffectiveEpiFamily.{u, u + 1, 0} (C := CompHaus) (B := profiniteToCompHaus.obj B)
      (fun (a : α) ↦ profiniteToCompHaus.obj (X a)) fun (a : α) ↦ profiniteToCompHaus.map (π a)) ↔
    EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
⊢ (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x :
        (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        (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)) (π a) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π

Tactic:
tfae_have 3 ↔ 1 := by
    erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)]
    exact ⟨fun h ↦ profiniteToCompHaus.finite_effectiveEpiFamily_of_map _ _ h,
      fun _ ↦ inferInstance⟩
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
tfae_3_iff_1 :
  (∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      ∃ (a : α) (x :
        (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        (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)) (π a) :
              (a :
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    (X a)) →
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  B)
            x =
          b) ↔
    EffectiveEpiFamily X π
⊢ [EffectiveEpiFamily X π, Epi (X := ∐ X) (Sigma.desc π),
      ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
        ∃ (a : α) (x :
          (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
          (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))
                  (π a) :
                (a :
                    (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                        (↑X.toTop : Type u))
                      (X a)) →
                  (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦
                      (↑X.toTop : Type u))
                    B)
              x =
            b].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Category.Profinite.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
surj :
  ∀ (b : (↑(B.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
    ∃ (a : α) (x : (↑((X a).toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)),
      (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)) (π a) :
            (a :
                (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                  (X a)) →
              (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u)) ↦ (↑X.toTop : Type u))
                B)
          x =
        b
⊢ EffectiveEpiFamily X π

Tactic:
((effectiveEpiFamily_tfae X π).out 2 0).mp surj

Premises used: List.TFAE.out, Iff.mp, OfNat.ofNat, Profinite.effectiveEpiFamily_tfae
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
⊢ DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))

Tactic:
have : DiscreteTopology (toProfinite.obj X) := ⟨rfl⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
this :
  DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
f' : LocallyConstant
  (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
    Type (max u w)) :=
  {
    toFun :=
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
                (↑X.toTop : Type (max u w)))
              c.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑X.toTop : Type (max u w)))
            (toProfinite.obj X)),
    isLocallyConstant := ⋯ }
obtain :
  ∀ (i : I)
    (g :
      LocallyConstant
        (↑(((F ⋙ toProfinite).obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max w u)))) :
          Type (max w u))
        (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
          Type (max u w)))
    (h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g),
    ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g
⊢ ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g

Tactic:
obtain ⟨i, g, h⟩ := exists_locallyConstant.{_, u} c hc f'
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
this :
  DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
f' : LocallyConstant
  (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
    Type (max u w)) :=
  {
    toFun :=
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
                (↑X.toTop : Type (max u w)))
              c.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑X.toTop : Type (max u w)))
            (toProfinite.obj X)),
    isLocallyConstant := ⋯ }
i : I
g :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max w u)))) :
      Type (max w u))
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
⊢ ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g

Tactic:
⟨i, ⟨↾g⟩, ?_⟩

Premises used: TypeCat.ofHom, Exists.intro, CategoryTheory.InducedCategory.Hom.mk, DFunLike.coe
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
X : FintypeCat
f : c.pt ⟶ toProfinite.obj X
x : TopologicalSpace X.obj := ⊥
this :
  DiscreteTopology
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
f' : LocallyConstant
  (↑(c.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))
  (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
    Type (max u w)) :=
  {
    toFun :=
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            C((↑(x1.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w)),
              (↑(x2.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))))
            (CC := fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
            (↑(X.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) : Type (max u w))) f) :
        (a :
            (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
                (↑X.toTop : Type (max u w)))
              c.pt) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w))) ↦
              (↑X.toTop : Type (max u w)))
            (toProfinite.obj X)),
    isLocallyConstant := ⋯ }
i : I
g :
  LocallyConstant
    (↑(((F ⋙ toProfinite).obj i).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max w u)))) :
      Type (max w u))
    (↑((toProfinite.obj X).toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u w)))) :
      Type (max u w))
h : f' = LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) g
refine :
  f =
    c.π.app i ≫
      toProfinite.map
        (InducedCategory.Hom.mk (F := ObjectProperty.FullSubcategory.obj)
          (↾(⇑g :
              (a : (↑((F ⋙ toProfinite).obj i).toTop : Type (max w u))) →
                (↑(toProfinite.obj X).toTop : Type (max u w)))))
⊢ ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g

Tactic:
refine ⟨i, ⟨↾g⟩, ?_⟩
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
suffices : (e.inverse ⋙ functor.{u, w} c).Initial
⊢ (functor.{u, w} c).Initial

Tactic:
suffices (e.inverse ⋙ functor c).Initial from initial_of_equivalence_comp e.inverse (functor c)
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
rw :
  (∀ (d : StructuredArrow c.pt toProfinite),
      ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)) ∧
    ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
      (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
      ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
        (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
⊢ (e.inverse ⋙ functor.{u, w} c).Initial

Tactic:
rw [initial_iff_of_isCofiltered (F := e.inverse ⋙ functor c)]

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.initial_iff_of_isCofiltered, Profinite.Extend.functor, CategoryTheory.Equivalence.inverse
-- Module: Mathlib.Topology.Category.Profinite.Extend
Goal:
I : Type u
inst : SmallCategory I
inst_1 : IsCofiltered I
F : I ⥤ FintypeCat
c : Cone (F ⋙ toProfinite)
hc : IsLimit c
inst_2 : ∀ (i : I), Epi (c.π.app i)
e : I ≌ ULiftHom (ULift.{w, u} I) := ULiftHomULiftCategory.equiv I
left :
  ∀ (d : StructuredArrow c.pt toProfinite),
    ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)
right :
  ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
    (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
    ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
      (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'
⊢ (∀ (d : StructuredArrow c.pt toProfinite),
      ∃ (c_1 : ULiftHom (ULift.{w, u} I)), Nonempty ((e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d)) ∧
    ∀ {d : StructuredArrow c.pt toProfinite} {c_1 : ULiftHom (ULift.{w, u} I)}
      (s s' : (e.inverse ⋙ functor.{u, w} c).obj c_1 ⟶ d),
      ∃ (c' : ULiftHom (ULift.{w, u} I)) (t : c' ⟶ c_1),
        (e.inverse ⋙ functor.{u, w} c).map t ≫ s = (e.inverse ⋙ functor.{u, w} c).map t ≫ s'

Tactic:
constructor