case w
C : Type u
inst✝³ : Category C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'
C : Type u
inst✝³ : Category C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'
apply image.ext
case w
C : Type u
inst✝³ : Category C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f =
    factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f')) ≫ ι f'
case w
C : Type u
inst✝³ : Category C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'
dsimp [asIso,image.eqToIso, image.eqToHom]
no goals
case w
C : Type u
inst✝³ : Category C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f =
    factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f')) ≫ ι f'
rw [image.lift_fac]