C : Type u
inst✝² : Category C
D : Type ?u.89599
inst✝¹ : Category D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective ((forget C).map (f ≫ g))
C : Type u
inst✝² : Category C
D : Type ?u.89599
inst✝¹ : Category D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ MorphismProperty.surjective C (f ≫ g)
delta MorphismProperty.surjective
C : Type u
inst✝² : Category C
D : Type ?u.89599
inst✝¹ : Category D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective ((forget C).map g ∘ (forget C).map f)
C : Type u
inst✝² : Category C
D : Type ?u.89599
inst✝¹ : Category D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective ((forget C).map (f ≫ g))
rw [coe_comp]
no goals
C : Type u
inst✝² : Category C
D : Type ?u.89599
inst✝¹ : Category D
inst✝ : ConcreteCategory C
X Y Z : C
f : X ⟶ Y
g : Y ⟶ Z
hf : MorphismProperty.surjective C f
hg : MorphismProperty.surjective C g
⊢ Surjective ((forget C).map g ∘ (forget C).map f)
exact hg.comp hf