awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
x : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))
⊢ Membership.mem (γ := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
      {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
        ∀ {i j : J} (f : i ⟶ j),
          (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                  C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                    (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                  (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                  (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                  (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
              (u i) =
            u j}
      x ↔
    Membership.mem (γ := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
      (⋂ (i : J),
        ⋂ (j : J),
          ⋂ (f : i ⟶ j),
            {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
              (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                      C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                        (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                      (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                      (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                    (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                      (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                  (u i) =
                u j})
      x

Tactic:
simp only [Set.mem_iInter, Set.mem_setOf_eq]

Premises used: Set.mem_setOf_eq, Set.mem_iInter
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
⊢ Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})

Tactic:
have :
          { u : ∀ j, F.obj j | ∀ {i j : J} (f : i ⟶ j), F.map f (u i) = u j } =
            ⋂ (i : J) (j : J) (f : i ⟶ j), { u | F.map f (u i) = u j } := by
          ext1
          simp only [Set.mem_iInter, Set.mem_setOf_eq]
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})
i j : J
f : i ⟶ j
⊢ Continuous (Y :=
    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      (F.obj j))
    fun (y : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) ↦
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
            (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
          (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
      (y i)

Tactic:
((F.map f).hom.hom.continuous).comp (continuous_apply i)

Premises used: ContinuousMap.continuous, Continuous.comp, CategoryTheory.Functor.map, TopCat.Hom.hom, continuous_apply, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})
i j : J
f : i ⟶ j
⊢ Continuous (Y :=
    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      (F.obj j))
    fun (y : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) ↦
    (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
          C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
            (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
          (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
          (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
        (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
          (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
      (y i)

Tactic:
exact ((F.map f).hom.hom.continuous).comp (continuous_apply i)

Premises used: ContinuousMap.continuous, Continuous.comp, CategoryTheory.Functor.map, TopCat.Hom.hom, CategoryTheory.InducedCategory.Hom.hom
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})
i j : J
f : i ⟶ j
⊢ Continuous (Y :=
    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      (F.obj j))
    fun (y : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) ↦ y j

Tactic:
continuous_apply j

Premises used: continuous_apply
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
this :
  Eq (α := Set ((j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
    {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
      ∀ {i j : J} (f : i ⟶ j),
        (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                  (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
              (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
            (u i) =
          u j}
    (⋂ (i : J),
      ⋂ (j : J),
        ⋂ (f : i ⟶ j),
          {u : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)) |
            (ConcreteCategory.hom (FC := fun (x1 x2 : CompHausLike fun (x : TopCat) ↦ True) ↦
                    C((↑(x1.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)),
                      (↑(x2.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))))
                    (CC := fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦
                    (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) (F.map f) :
                  (a : (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj i)) →
                    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑X.toTop : Type (max u v))) (F.obj j))
                (u i) =
              u j})
i j : J
f : i ⟶ j
⊢ Continuous (Y :=
    (fun (X : CompHausLike fun (x : TopCat) ↦ True) ↦ (↑(X.toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v)))
      (F.obj j))
    fun (y : (j : J) → (↑((F.obj j).toTop (P := fun (x : TopCat) ↦ True)) : Type (max u v))) ↦ y j

Tactic:
exact continuous_apply j

Premises used: continuous_apply
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
X : J
_ :
  ∀ ⦃Y : J⦄ (f : X ⟶ Y),
    Eq (α :=
      Functor.obj
          (Functor.obj (Functor.const J) (mk (P := fun (x : TopCat) ↦ True) (TopCat.limitCone.{v, u, v} FF).pt trivial))
          X ⟶
        F.obj Y)
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const J) (mk (P := fun (x : TopCat) ↦ True) (TopCat.limitCone.{v, u, v} FF).pt trivial))
          f ≫
        InducedCategory.homMk ((TopCat.limitCone.{v, u, v} FF).π.app Y))
      (InducedCategory.homMk ((TopCat.limitCone.{v, u, v} FF).π.app X) ≫ F.map f)
⊢ ∀ ⦃Y : J⦄ (f : X ⟶ Y),
    Eq (α :=
      Functor.obj
          (Functor.obj (Functor.const J) (mk (P := fun (x : TopCat) ↦ True) (TopCat.limitCone.{v, u, v} FF).pt trivial))
          X ⟶
        F.obj Y)
      (CategoryTheory.Functor.map
          (Functor.obj (Functor.const J) (mk (P := fun (x : TopCat) ↦ True) (TopCat.limitCone.{v, u, v} FF).pt trivial))
          f ≫
        InducedCategory.homMk ((TopCat.limitCone.{v, u, v} FF).π.app Y))
      (InducedCategory.homMk ((TopCat.limitCone.{v, u, v} FF).π.app X) ≫ F.map f)

Tactic:
_
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
S : Limits.Cone F
m : S.pt ⟶ (limitCone.{v, u} F).pt
hm : ∀ (j : J), m ≫ (limitCone.{v, u} F).π.app j = S.π.app j
j : J
simp : m.hom ≫ (TopCat.limitCone.{v, u, v} FF).π.app j = (m ≫ (limitCone.{v, u} F).π.app j).hom
⊢ m.hom ≫ (TopCat.limitCone.{v, u, v} FF).π.app j = (compHausToTop.mapCone S).π.app j

Tactic:
simp [← hm]
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
J : Type v
inst : SmallCategory J
F : J ⥤ CompHaus
FF : J ⥤ TopCat := F ⋙ compHausToTop
S : Limits.Cone F
m : S.pt ⟶ (limitCone.{v, u} F).pt
hm : ∀ (j : J), m ≫ (limitCone.{v, u} F).π.app j = S.π.app j
j : J
⊢ m.hom ≫ (TopCat.limitCone.{v, u, v} FF).π.app j = (m ≫ (limitCone.{v, u} F).π.app j).hom

Tactic:
rfl
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X Y : CompHaus
f : X ⟶ Y
mp :
  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)
mpr :
  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
⊢ 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)

Tactic:
constructor
-- Module: Mathlib.Topology.Category.CompHaus.Basic
Goal:
X Y : CompHaus
f : X ⟶ Y
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
⊢ 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

Tactic:
contrapose!
-- 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)
⊢ IsClosed C

Tactic:
have hC : IsClosed C := (isCompact_range f.hom.hom.continuous).isClosed
-- 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}
⊢ IsClosed D

Tactic:
have hD : IsClosed D := isClosed_singleton