X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ((forget TopCat).map f)
suffices Epi f ↔ Epi ((forget TopCat).map f) by
  rw [this, CategoryTheory.epi_iff_surjective]
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)

case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)
constructor
no goals
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Epi f ↔ Function.Surjective ((forget TopCat).map f)
rw [this, CategoryTheory.epi_iff_surjective]
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)
intro
no goals
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
infer_instance
no goals
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f
apply Functor.epi_of_epi_map