Lean4
/-- the universal property for the image factorisation -/
noncomputable def lift (F' : MonoFactorisation f) : image f ⟶ F'.I :=
ofHom
{ toFun := (fun x => F'.e (Classical.indefiniteDescription _ x.2).1 : image f → F'.I)
map_zero' := by
haveI := F'.m_mono
apply injective_of_mono F'.m
change (F'.e ≫ F'.m) _ = _
rw [F'.fac, AddMonoidHom.map_zero]
exact (Classical.indefiniteDescription (fun y => f y = 0) _).2
map_add' := by
intro x y
haveI := F'.m_mono
apply injective_of_mono F'.m
rw [AddMonoidHom.map_add]
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _
rw [F'.fac]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
rw [(Classical.indefiniteDescription (fun z => f z = _) _).2]
rfl }
