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