awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
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'
⊢ 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 := ⋯ }
have 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 := sorry :
              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 :
      α)
Tactic: ext1 t
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (hypothesis)
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.{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 :
      α)
have hj₁ : 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
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
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)
t : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hj :
  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)
⊢ 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 :
      α)
have inr : (f : (a : (↑C.pt.toTop : Type (max u v))) → α) t =
  ff
    ((g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid)
      ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v))) t))
Tactic: dsimp at hj ⊢
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.CofilteredLimit (goal)
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)
t : (↑(C.pt.toTop (P := fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type (max u v)))) : Type (max u v))
hj :
  Eq (α := Quotient S.toSetoid)
    ((f' : (a : (↑C.pt.toTop : Type (max u v))) → Quotient S.toSetoid) t : Quotient S.toSetoid)
    ((g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid)
        ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
          t) :
      Quotient S.toSetoid)
⊢ (f : (a : (↑C.pt.toTop : Type (max u v))) → α) t =
    ff
      ((g' : (a : (↑(F.obj j).toTop : Type (max u v))) → Quotient S.toSetoid)
        ((TopCat.Hom.hom (C.π.app j).hom : (a : (↑C.pt.toTop : Type (max u v))) → (↑(F.obj j).toTop : Type (max u v)))
          t))
have inr : (f : (a : (↑C.pt.toTop : Type (max u v))) → α) t =
  ff ((f' : (a : (↑C.pt.toTop : Type (max u v))) → Quotient S.toSetoid) t)
Tactic: rw [← hj]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (hypothesis)
Goal:
B X : Profinite
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π,
      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))
          B)
        (⇑(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 :
              (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))
              B)].TFAE
have tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (hypothesis)
Goal:
B X : Profinite
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ [EffectiveEpi π, Epi π,
      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))
          B)
        (⇑(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 :
              (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))
              B)].TFAE
have tfae_2_iff_3 : Epi π ↔
  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))
      B)
    (⇑(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 : (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)) B)
Tactic: tfae_have 2 ↔ 3 := epi_iff_surjective π
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (hypothesis)
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
⊢ [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
have tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), EffectiveEpiFamily X π
Tactic: tfae_have 2 → 1
  | _ => by
    simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (hypothesis)
Goal:
α : Type
inst : Finite α
B : Profinite
X : α → Profinite
π : (a : α) → X a ⟶ B
tfae_2_to_1 : ∀ (a : Epi (X := ∐ X) (Sigma.desc π)), 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
have tfae_1_to_2 : ∀ (a : EffectiveEpiFamily X π), Epi (X := ∐ X) (Sigma.desc π)
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (goal)
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 π
have 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 π
Tactic: erw [((CompHaus.effectiveEpiFamily_tfae
      (fun a ↦ profiniteToCompHaus.obj (X a)) (fun a ↦ profiniteToCompHaus.map (π a))).out 2 0 :)]
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.EffectiveEpi (hypothesis)
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 π, 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
have 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 π
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⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (hypothesis)
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 := ⊥
⊢ ∃ (i : I) (g : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g
have this : 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⟩
-- Lean 4 proof step from Mathlib.Topology.Category.Profinite.Extend (goal)
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 : F.obj i ⟶ X), f = c.π.app i ≫ toProfinite.map g
have 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
Tactic: obtain ⟨i, g, h⟩ := exists_locallyConstant.{_, u} c hc f'