C : Type u
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f
C : Type u
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ f = image.ι f
simp only [← imageMonoIsoSource_inv_ι f]
no goals
C : Type u
inst✝¹ : Category C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]