awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
⊢ Epi f →
    ∀ (b : (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
      ∃ (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 =
          b
have mp : (∃ (b : (↑(Y.toTop (P := fun (x : TopCat.{u}) ↦ True)) : Type u)),
    ∀ (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 ≠
        b) →
  ¬Epi f
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
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)
⊢ False
have hC : IsClosed C
Tactic: have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
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}
⊢ False
have hD : IsClosed D
Tactic: have hD : IsClosed D := isClosed_singleton
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
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
⊢ Disjoint C D
have rw : y ∉ C
Tactic: rw [Set.disjoint_singleton_right]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
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
⊢ False
have hCD : Disjoint C D
Tactic: have hCD : Disjoint C D := by
      rw [Set.disjoint_singleton_right]
      rintro ⟨y', hy'⟩
      exact hy y' hy'
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
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
⊢ False
have mp : ∀
  (φ :
    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 : ℝ)),
  False
Tactic: obtain ⟨φ, hφ0, hφ1, hφ01⟩ := exists_continuous_zero_one_of_isClosed hC hD hCD
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
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 : ℝ)
⊢ False
have this : CompactSpace.{u} (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
Tactic: haveI : CompactSpace (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.compactSpace
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (hypothesis)
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 : CompactSpace.{u} (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
⊢ False
have this₁ : T2Space.{u} (ULift.{u, 0} (↑(Set.Icc 0 1) : Type))
Tactic: haveI : T2Space (ULift.{u} <| Set.Icc (0 : ℝ) 1) := Homeomorph.ulift.symm.t2Space
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
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 = g
have rw : f ≫ h = f ≫ g
Tactic: rw [← cancel_epi f]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.Basic (goal)
Goal:
X Y : CompHaus
f : X ⟶ Y
⊢ 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
have 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
Tactic: rw [← CategoryTheory.ofHom_epi_iff_surjective]
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.EffectiveEpi (hypothesis)
Goal:
B X : CompHaus
π : X ⟶ B
⊢ [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
have tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
Tactic: tfae_have 1 → 2 := fun _ ↦ inferInstance
-- Lean 4 proof step from Mathlib.Topology.Category.CompHaus.EffectiveEpi (hypothesis)
Goal:
B X : CompHaus
π : X ⟶ B
tfae_1_to_2 : ∀ (a : EffectiveEpi π), Epi π
⊢ [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
have 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)
Tactic: tfae_have 2 ↔ 3 := epi_iff_surjective π