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