-- Mathlib/CategoryTheory/ConcreteCategory/EpiMono.lean
lemma surjective_eq_epimorphisms_iff :
    MorphismProperty.surjective C = epimorphisms C ↔ (forget C).PreservesEpimorphisms

Proof state:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [inst : Epi f], Epi ((forget C).map f)

Tactic:
rintro _ _ f (hf : epimorphisms C f)

Result:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Epi ((forget C).map f)

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.surjective C = epimorphisms C → (forget C).PreservesEpimorphisms

Tactic:
intro h

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ (forget C).PreservesEpimorphisms

Proof state:
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.surjective C = epimorphisms C ↔ (forget C).PreservesEpimorphisms

Tactic:
constructor

Result:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ MorphismProperty.surjective C = epimorphisms C → (forget C).PreservesEpimorphisms

case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ (forget C).PreservesEpimorphisms → MorphismProperty.surjective C = epimorphisms C

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ MorphismProperty.surjective C f

Tactic:
change Function.Surjective ((forget C).map f)

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Function.Surjective ((forget C).map f)

Proof state:
case mp
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ (forget C).PreservesEpimorphisms

Tactic:
constructor

Result:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
⊢ ∀ {X Y : C} (f : X ⟶ Y) [inst : Epi f], Epi ((forget C).map f)

Proof state:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ Function.Surjective ((forget C).map f)

Tactic:
rw [← h] at hf

Result:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ((forget C).map f)

Proof state:
case mp.preserves
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
h : MorphismProperty.surjective C = epimorphisms C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : MorphismProperty.surjective C f
⊢ Function.Surjective ((forget C).map f)

Tactic:
exact hf

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
⊢ epimorphisms C ≤ MorphismProperty.surjective C

Tactic:
intro _ _ f hf

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ MorphismProperty.surjective C f

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
⊢ MorphismProperty.surjective C f

Tactic:
have : Epi f := hf

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ MorphismProperty.surjective C f

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Function.Surjective ((forget C).map f)

Tactic:
rw [← epi_iff_surjective]

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Epi ((forget C).map f)

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : epimorphisms C f
this : Epi f
⊢ Epi ((forget C).map f)

Tactic:
infer_instance

Result:
no goals

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
⊢ (forget C).PreservesEpimorphisms → MorphismProperty.surjective C = epimorphisms C

Tactic:
intro

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
⊢ MorphismProperty.surjective C = epimorphisms C

Proof state:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
⊢ MorphismProperty.surjective C = epimorphisms C

Tactic:
apply le_antisymm (surjective_le_epimorphisms C)

Result:
case mpr
C : Type u
inst✝² : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type w
inst✝¹ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝ : ConcreteCategory C FC
a✝ : (forget C).PreservesEpimorphisms
⊢ epimorphisms C ≤ MorphismProperty.surjective C