C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.epimorphisms C f
hg : MorphismProperty.epimorphisms C g
⊢ MorphismProperty.epimorphisms C (f ≫ g)
rw [epimorphisms.iff] at hf hg⊢
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this : Epi f
⊢ Epi (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
⊢ Epi (f ≫ g)
haveI := hf
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this✝ : Epi f
this : Epi g
⊢ Epi (f ≫ g)
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this : Epi f
⊢ Epi (f ≫ g)
haveI := hg
no goals
C : Type u
inst✝¹ : Category C
D : Type ?u.64328
inst✝ : Category D
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : Epi f
hg : Epi g
this✝ : Epi f
this : Epi g
⊢ Epi (f ≫ g)
apply epi_comp