awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
this :
  Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation))
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
        (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1))
      (profiniteToCompHaus.obj X))
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1),
            (↑(x2.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u_1}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u_1}) ↦ True)) : Type u_1)) (X :=
          ProjectivePresentation.p (X := profiniteToCompHaus.obj X) (profiniteToCompHaus.obj X).projectivePresentation)
          (ProjectivePresentation.f (profiniteToCompHaus.obj X).projectivePresentation)) :
      (a :
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1))
            (profiniteToCompHaus.obj X).projectivePresentation.p) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u_1)) (profiniteToCompHaus.obj X))
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
      (Stonean.toProfinite.obj X.presentation))
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
      X)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1),
            (↑(x2.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u_1}) ↦ TotallyDisconnectedSpace.{u_1} (↑X : Type u_1))) : Type u_1))
          (π X)) :
      (a :
          (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1))
            (Stonean.toProfinite.obj X.presentation)) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ TotallyDisconnectedSpace (↑X : Type u_1)) ↦ (↑X.toTop : Type u_1)) X)

Tactic:
exact this
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X Y : Profinite
Z : Stonean
e : Stonean.toProfinite.obj Z ⟶ Y
f : X ⟶ Y
inst : Epi f
⊢ lift e f ≫ f = e

Tactic:
simp [lift]

Premises used: Profinite.lift
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
hX :
  ExtremallyDisconnected.{u}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
change :
  Projective
    (Stonean.toProfinite.obj
      (CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
        (X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) ⋯))
⊢ Projective X

Tactic:
change Projective (Stonean.toProfinite.obj ⟨X.toTop, inferInstance⟩)

Premises used: Stonean.toProfinite, inferInstance, CompHausLike.mk, CategoryTheory.Projective, CompHausLike.toTop, CategoryTheory.Functor.obj
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
hX :
  ExtremallyDisconnected.{u}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Projective
    (Stonean.toProfinite.obj
      (CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
        (X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) ⋯))

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Stonean.Basic
Goal:
X : Profinite
hX :
  ExtremallyDisconnected.{u}
    (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) : Type u)
⊢ Projective
    (Stonean.toProfinite.obj
      (CompHausLike.mk (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))
        (X.toTop (P := fun (X : TopCat.{u}) ↦ TotallyDisconnectedSpace.{u} (↑X : Type u))) ⋯))

Tactic:
exact inferInstance
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
⊢ EffectiveEpi π

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
⊢ Epi π

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
⊢ ∀ (a : EffectiveEpi π), Epi π

Tactic:
1 → 2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
⊢ ∀ (a : EffectiveEpi π), Epi π

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Epi π

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
      X)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
      B)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)

Tactic:
2 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Premises used: Stonean.epi_iff_surjective
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
tfae_2_iff_3 :
  Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
      X)
    (β :=
    (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
        (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
      B)
    (⇑(ConcreteCategory.hom (FC :=
          fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
            (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
          (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
      (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
tfae_2_iff_3 :
  Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ EffectiveEpi π

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
tfae_2_iff_3 :
  Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ ∀
    (a :
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          X)
        (β :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          B)
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)),
    EffectiveEpi π

Tactic:
3 → 1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
tfae_2_iff_3 :
  Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        X)
      (β :=
      (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
          (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
        B)
      (⇑(ConcreteCategory.hom (FC :=
            fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
              (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
            (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)
⊢ ∀
    (a :
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          X)
        (β :=
        (fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
            (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u))
          B)
        (⇑(ConcreteCategory.hom (FC :=
              fun (x1 x2 : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              C((↑(x1.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u),
                (↑(x2.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)))
              (CC := fun (X : CompHausLike fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u)) ↦
              (↑(X.toTop (P := fun (X : TopCat.{u}) ↦ ExtremallyDisconnected.{u} (↑X : Type u))) : Type u)) π) :
          (a :
              (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u))
                X) →
            (fun (X : CompHausLike fun (X : TopCat) ↦ ExtremallyDisconnected (↑X : Type u)) ↦ (↑X.toTop : Type u)) B)),
    EffectiveEpi π

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
⊢ Preregular Stonean

Tactic:
Stonean.toCompHaus.reflects_preregular

Premises used: Stonean.toCompHaus, CategoryTheory.Functor.reflects_preregular
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
⊢ Precoherent Stonean

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
⊢ 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.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π

Tactic:
1

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

Tactic:
2 → 1

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

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Topology.Category.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (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.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (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.Stonean.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : Stonean
X : α → Stonean
π : (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