awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X Y : CompHaus
f : X ⟶ Y
y : (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)
hy :
  ∀ (a : (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f :
          (a : (↑X.toTop : Type u)) → (↑Y.toTop : Type u))
        a ≠
      y
hf : Epi f
C : Set
  ((fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y) :=
  Set.range (ι :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)
hC : IsClosed C
D : Set (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u) := {y}
hD : IsClosed D
hCD : Disjoint C D
φ :
  C((fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y,
    ℝ)
hφ0 : Set.EqOn (β := ℝ) (⇑φ : (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) → ℝ) 0 C
hφ1 : Set.EqOn (β := ℝ) (⇑φ : (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) → ℝ) 1 D
hφ01 :
  ∀
    (x :
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
        Y),
    Membership.mem (α := ℝ) (γ := Set ℝ) (Set.Icc 0 1)
      ((φ : (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) → ℝ) x : ℝ)
this_1 : CompactSpace.{u} (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
this : T2Space.{u} (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
Z : CompHaus := of (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
g : Y ⟶ Z :=
  ofHom (fun (x : TopCat.{u}) ↦ True)
    {
      toFun := fun (y' : (↑Y.1 : Type u)) ↦
        {
          down :=
            Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x)
              ((φ : (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) → ℝ) y') ⋯ },
      continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun (x : TopCat.{u}) ↦ True)
    {
      toFun := fun (x : (↑Y.1 : Type u)) ↦
        { down := Subtype.mk (p := fun (x : ℝ) ↦ Membership.mem (γ := Set ℝ) (Set.Icc 0 1) x) 0 ⋯ },
      continuous_toFun := ⋯ }
H : Eq (α := ℝ) 0 1
⊢ False

Tactic:
exact zero_ne_one H

Premises used: zero_ne_one
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X Y : CompHaus
f : X ⟶ Y
mpr :
  Epi (X :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (Y :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)) →
    Epi f
⊢ Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y) →
    Epi f

Tactic:
rw [← CategoryTheory.ofHom_epi_iff_surjective]

Premises used: CategoryTheory.ofHom_epi_iff_surjective
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X Y : CompHaus
f : X ⟶ Y
⊢ Epi (X :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (Y :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) Y)
      (↾(⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) f) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) Y)) →
    Epi f

Tactic:
apply (forget CompHaus).epi_of_epi_map

Premises used: CategoryTheory.forget, CategoryTheory.Functor.epi_of_epi_map, CompHaus
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
P : TopCat.{u_1} → Prop
⊢ ∀ (X : CompHausLike P), P (X.toTop (P := P)) → True

Tactic:
simp only [implies_true]

Premises used: implies_true
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : 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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : 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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : 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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : X ⟶ B
⊢ ∀ (a : EffectiveEpi π), Epi π

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : 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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Function.Surjective (α :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
    (β :=
    (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B)
    (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
            (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
          (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
      (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
        (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑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.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

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

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
tfae_2_iff_3 :
  Epi π ↔
    Function.Surjective (α :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) X)
      (β :=
      (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) B)
      (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
              (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
            (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
            (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)
tfae_3_to_1 :
  ∀
    (a :
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          X)
        (β :=
        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)),
    EffectiveEpi π
⊢ [EffectiveEpi π, Epi π,
      Function.Surjective (α :=
        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          X)
        (β :=
        (fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u))
          B)
        (⇑(ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              C((↑(x1.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u),
                (↑(x2.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)))
              (CC := fun (X : CompHausLike fun (x : TopCat.{u}) ↦ True) ↦
              (↑(X.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)) π) :
          (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) X) →
            (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type u)) B)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
⊢ Preregular CompHaus

Tactic:
preregular fun _ _ _ ↦ ((effectiveEpi_tfae _).out 0 2).mp

Premises used: List.TFAE.out, CompHaus.effectiveEpi_tfae, Iff.mp, OfNat.ofNat, CompHausLike.preregular
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
⊢ Precoherent CompHaus

Tactic:
inferInstance

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

Tactic:
simpa [← effectiveEpi_desc_iff_effectiveEpiFamily, (effectiveEpi_tfae (Sigma.desc π)).out 0 1]

Premises used: List.TFAE.out, CompHaus.effectiveEpi_tfae, CategoryTheory.effectiveEpi_desc_iff_effectiveEpiFamily, CategoryTheory.Limits.Sigma.desc, OfNat.ofNat
-- Module: Mathlib.Topology.Category.CompHaus.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (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.CompHaus.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (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.CompHaus.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (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.CompHaus.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (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.CompHaus.EffectiveEpi
Goal:
α : Type
inst : Finite α
B : CompHaus
X : α → CompHaus
π : (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
  | _ => inferInstance