case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
⊢ ∀ {X Y Z : C} (e : Y ≅ Z) (f : X ⟶ Y), MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
intro X Y Z e f
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Epi f → Epi (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ MorphismProperty.epimorphisms C f → MorphismProperty.epimorphisms C (f ≫ e.hom)
simp only [epimorphisms.iff]
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : Epi f
⊢ Epi (f ≫ e.hom)
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
⊢ Epi f → Epi (f ≫ e.hom)
intro
no goals
case right
C : Type u
inst✝¹ : Category C
D : Type ?u.61126
inst✝ : Category D
X Y Z : C
e : Y ≅ Z
f : X ⟶ Y
a✝ : Epi f
⊢ Epi (f ≫ e.hom)
apply epi_comp