C : Type u
inst✝ : Category C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage F) hF').hom)
C : Type u
inst✝ : Category C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
no goals
C : Type u
inst✝ : Category C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage F) hF').hom)
apply strongEpi_comp