C : Type u₁
inst✝ : Category C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono (IsInitial.to hI' X)
C : Type u₁
inst✝ : Category C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono (IsInitial.to hI' X)
dsimp
C : Type u₁
inst✝ : Category C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((IsInitial.uniqueUpToIso hI' hI).hom ≫ IsInitial.to hI X)
C : Type u₁
inst✝ : Category C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono (IsInitial.to hI' X)
rw [hI'.hom_ext (hI'.to X) ((hI'.uniqueUpToIso hI).hom ≫ hI.to X)]
no goals
C : Type u₁
inst✝ : Category C
I : C
hI : IsInitial I
h : ∀ (X : C), Mono (IsInitial.to hI X)
I' X : C
hI' : IsInitial I'
⊢ Mono ((IsInitial.uniqueUpToIso hI' hI).hom ≫ IsInitial.to hI X)
apply mono_comp