C : Type u₁
inst✝¹ : Category C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (to hI X)
C : Type u₁
inst✝¹ : Category C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono f
rw [hI.hom_ext f (hI.to X)]
no goals
C : Type u₁
inst✝¹ : Category C
inst✝ : InitialMonoClass C
I X : C
hI : IsInitial I
f : I ⟶ X
⊢ Mono (to hI X)
apply InitialMonoClass.isInitial_mono_from