[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
suffices Epi f ↔ Epi ((forget TopCat).map f)
  by
  rw [this, CategoryTheory.epi_iff_surjective]
  rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Epi f ↔ Function.Surjective ↑f
[PROOFSTEP]
rw [this, CategoryTheory.epi_iff_surjective]
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Epi f ↔ Epi ((forget TopCat).map f)
⊢ Function.Surjective ((forget TopCat).map f) ↔ Function.Surjective ↑f
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Epi f ↔ Epi ((forget TopCat).map f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Epi f → Epi ((forget TopCat).map f)
[PROOFSTEP]
intro
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Epi f
⊢ Epi ((forget TopCat).map f)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Epi ((forget TopCat).map f) → Epi f
[PROOFSTEP]
apply Functor.epi_of_epi_map
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
suffices Mono f ↔ Mono ((forget TopCat).map f)
  by
  rw [this, CategoryTheory.mono_iff_injective]
  rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Mono f ↔ Function.Injective ↑f
[PROOFSTEP]
rw [this, CategoryTheory.mono_iff_injective]
[GOAL]
X Y : TopCat
f : X ⟶ Y
this : Mono f ↔ Mono ((forget TopCat).map f)
⊢ Function.Injective ((forget TopCat).map f) ↔ Function.Injective ↑f
[PROOFSTEP]
rfl
[GOAL]
X Y : TopCat
f : X ⟶ Y
⊢ Mono f ↔ Mono ((forget TopCat).map f)
[PROOFSTEP]
constructor
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
⊢ Mono f → Mono ((forget TopCat).map f)
[PROOFSTEP]
intro
[GOAL]
case mp
X Y : TopCat
f : X ⟶ Y
a✝ : Mono f
⊢ Mono ((forget TopCat).map f)
[PROOFSTEP]
infer_instance
[GOAL]
case mpr
X Y : TopCat
f : X ⟶ Y
⊢ Mono ((forget TopCat).map f) → Mono f
[PROOFSTEP]
apply Functor.mono_of_mono_map
