C : Type u
inst✝³ : Category C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ IsImage.lift (StrongEpiMonoFactorisation.toMonoIsImage (StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e)))
        (Image.monoFactorisation f) ≫
      ι f =
    m
C : Type u
inst✝³ : Category C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (isoStrongEpiMono e m comm).hom ≫ ι f = m
dsimp [isoStrongEpiMono]
no goals
C : Type u
inst✝³ : Category C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ IsImage.lift (StrongEpiMonoFactorisation.toMonoIsImage (StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e)))
        (Image.monoFactorisation f) ≫
      ι f =
    m
apply IsImage.lift_fac