awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))

Tactic:
isOpenEmbedding_iff_isIso_comp f g

Premises used: TopCat.isOpenEmbedding_iff_isIso_comp
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y Z : TopCat
f : X ⟶ Y
g : Y ⟶ Z
inst : IsIso f
⊢ IsOpenEmbedding (X := (↑X : Type u)) (Y := (↑Z : Type u))
      (Function.comp (β := (↑Y : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑X : Type u)) → (↑Y : Type u))) ↔
    IsOpenEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
        (a : (↑Y : Type u)) → (↑Z : Type u))

Tactic:
exact isOpenEmbedding_iff_isIso_comp f g

Premises used: TopCat.isOpenEmbedding_iff_isIso_comp
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
A X : TopCat
f : A ⟶ X
⊢ isEmbedding f ↔
    IsEmbedding (X := (↑A : Type u_1)) (Y := (↑X : Type u_1)) (⇑(Hom.hom f) : (a : (↑A : Type u_1)) → (↑X : Type u_1))

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
y : (↑Y : Type u)
⊢ Continuous (Y := (↑Y : Type u)) fun (x : (↑X : Type u)) ↦ y

Tactic:
fun_prop
-- Module: Mathlib.Topology.Category.TopCat.Basic
Goal:
X Y : TopCat
y : (↑Y : Type u)
x : (↑X : Type u)
⊢ (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X := X)
          (const y) :
        (a : (↑X : Type u)) → (↑Y : Type u))
      x =
    y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
w :
  ∀ (x : (↑(of (↑X : Type u)) : Type u)),
    Eq (α := (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
⊢ Eq (α := of (↑X : Type u) ⟶ B) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
x : (↑(of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))

Tactic:
hab
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
x : (↑(of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))

Tactic:
exact hab
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
w :
  ∀ (x : (↑(of (↑X : Type u)) : Type u)),
    Eq (α := (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
              of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
            (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
          x :
        (↑B : Type u))
⊢ Eq (α := of (↑X : Type u) ⟶ B) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π)
    (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π)

Tactic:
ext
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
x : (↑(of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))

Tactic:
hab
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a b : (↑X : Type u)
hab :
  Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        a :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
          (a : (↑X : Type u)) → (↑B : Type u))
        b :
      (↑B : Type u))
x : (↑(of (↑X : Type u)) : Type u)
⊢ Eq (α := (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ a, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            of (↑X : Type u)) (ofHom { toFun := fun (x : (↑X : Type u)) ↦ b, continuous_toFun := ⋯ } ≫ π) :
          (a : (↑(of (↑X : Type u)) : Type u)) → (↑B : Type u))
        x :
      (↑B : Type u))

Tactic:
exact hab
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
this :
  g =
    ofHom
      ((hπ.liftEquiv :
          (a :
              { g : C((↑X : Type u), (↑W : Type u)) //
                Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
            C((↑B : Type u), (↑W : Type u)))
        (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
          Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
            (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  π) :
              (a : (↑X : Type u)) → (↑B : Type u)))
          (Hom.hom e) ⋯))
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
assumption
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
suffices :
  g =
    ofHom
      ((hπ.liftEquiv :
          (a :
              { g : C((↑X : Type u), (↑W : Type u)) //
                Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
            C((↑B : Type u), (↑W : Type u)))
        (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
          Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
            (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  π) :
              (a : (↑X : Type u)) → (↑B : Type u)))
          (Hom.hom e) ⋯))
⊢ g = ofHom (hπ.lift (Hom.hom e) ⋯)

Tactic:
suffices g = ofHom (hπ.liftEquiv ⟨e.hom,
      fun a b hab ↦ CategoryTheory.congr_fun (h
          (ofHom ⟨fun _ ↦ a, continuous_const⟩)
          (ofHom ⟨fun _ ↦ b, continuous_const⟩)
          (by ext; exact hab))
        a⟩) by assumption
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
hf :
  Hom.hom g =
    Hom.hom
      (ofHom
        ((hπ.liftEquiv :
            (a :
                { g : C((↑X : Type u), (↑W : Type u)) //
                  Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                    (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
              C((↑B : Type u), (↑W : Type u)))
          (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
            Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
              (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
              (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                    π) :
                (a : (↑X : Type u)) → (↑B : Type u)))
            (Hom.hom e) ⋯)))
⊢ g =
    ofHom
      ((hπ.liftEquiv :
          (a :
              { g : C((↑X : Type u), (↑W : Type u)) //
                Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) }) →
            C((↑B : Type u), (↑W : Type u)))
        (Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
          Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
            (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
                  π) :
              (a : (↑X : Type u)) → (↑B : Type u)))
          (Hom.hom e) ⋯))

Tactic:
apply hom_ext

Premises used: TopCat.hom_ext
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a : (↑X : Type u)
hf :
  Eq (α := (↑W : Type u))
    ((Hom.hom g : (a : (↑B : Type u)) → (↑W : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
              (a : (↑X : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      (↑W : Type u))
    ((Hom.hom (π ≫ g) : (a : (↑X : Type u)) → (↑W : Type u)) a : (↑W : Type u))
⊢ Eq (α := (↑W : Type u))
    (((↑((Equiv.symm hπ.liftEquiv :
                  (a : C((↑B : Type u), (↑W : Type u))) →
                    { g : C((↑X : Type u), (↑W : Type u)) //
                      Function.FactorsThrough (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                        (⇑(ConcreteCategory.hom π) : (a : (↑X : Type u)) → (↑B : Type u)) })
                (Hom.hom g)) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))
    (((↑(Subtype.mk (p := fun (g : C((↑X : Type u), (↑W : Type u))) ↦
                Function.FactorsThrough (α := (↑X : Type u)) (β := (↑B : Type u)) (γ := (↑W : Type u))
                  (⇑g : (a : (↑X : Type u)) → (↑W : Type u))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) π) :
                    (a : (↑X : Type u)) → (↑B : Type u)))
                (Hom.hom e) ⋯) :
            C((↑X : Type u), (↑W : Type u))) :
          (a : (↑X : Type u)) → (↑W : Type u))
        a :
      (↑W : Type u))

Tactic:
simp only [IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply, ← hm]

Premises used: Topology.IsQuotientMap.liftEquiv_symm_apply_coe, ContinuousMap.comp_apply
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
hπ :
  IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))
W : TopCat
e : X ⟶ W
h : ∀ {Z : TopCat.{u}} (g₁ g₂ : Z ⟶ X), g₁ ≫ π = g₂ ≫ π → g₁ ≫ e = g₂ ≫ e
g : B ⟶ W
hm : π ≫ g = e
a : (↑X : Type u)
⊢ Eq (α := (↑W : Type u))
    ((Hom.hom g : (a : (↑B : Type u)) → (↑W : Type u))
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π :
              (a : (↑X : Type u)) → (↑B : Type u))
            a :
          (↑B : Type u)) :
      (↑W : Type u))
    ((Hom.hom (π ≫ g) : (a : (↑X : Type u)) → (↑W : Type u)) a : (↑W : Type u))

Tactic:
rfl
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
⊢ EffectiveEpi π ↔
    IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
        (a : (↑X : Type u)) → (↑B : Type u))

Tactic:
⟨fun _ ↦ ?_, fun hπ ↦ ⟨⟨effectiveEpiStructOfQuotientMap π hπ⟩⟩⟩

Premises used: Nonempty.intro, TopCat.effectiveEpiStructOfQuotientMap, Iff.intro, CategoryTheory.EffectiveEpi.mk
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
refine :
  EffectiveEpi π →
    IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
        (a : (↑X : Type u)) → (↑B : Type u))
⊢ EffectiveEpi π ↔
    IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
        (a : (↑X : Type u)) → (↑B : Type u))

Tactic:
refine ⟨fun _ ↦ ?_, fun hπ ↦ ⟨⟨effectiveEpiStructOfQuotientMap π hπ⟩⟩⟩
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
h : EffectiveEpi π
⊢ IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))

Tactic:
isQuotientMap_of_isColimit_cofork _ (IsRegularEpi.isColimit π)

Premises used: CategoryTheory.IsRegularEpi.isColimit, TopCat.isQuotientMap_of_isColimit_cofork
-- Module: Mathlib.Topology.Category.TopCat.EffectiveEpi
Goal:
B X : TopCat
π : X ⟶ B
h : EffectiveEpi π
⊢ IsQuotientMap (X := (↑X : Type u)) (Y := (↑B : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) π) :
      (a : (↑X : Type u)) → (↑B : Type u))

Tactic:
exact isQuotientMap_of_isColimit_cofork _ (IsRegularEpi.isColimit π)

Premises used: CategoryTheory.IsRegularEpi.isColimit, TopCat.isQuotientMap_of_isColimit_cofork
-- Module: Mathlib.Topology.Category.TopCat.EpiMono
Goal:
X Y : TopCat
f : X ⟶ Y
this :
  Epi f ↔
    Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f)
rw :
  Epi (X :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (CategoryTheory.Functor.map
        (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) f) ↔
    Function.Surjective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))
rw₁ rw₂ :
  Function.Surjective (α :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) X)
      (β :=
      Functor.obj (forget TopCat (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)) Y)
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u)) ↔
    Function.Surjective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))
⊢ Epi f ↔
    Function.Surjective (α := (↑X : Type u)) (β := (↑Y : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
        (a : (↑X : Type u)) → (↑Y : Type u))

Tactic:
rw [this, CategoryTheory.ofHom_epi_iff_surjective]

Premises used: CategoryTheory.ofHom_epi_iff_surjective