chore(category_theory/images): fix some minor problems (#2182)

* chore(category_theory/images): fix some minor problems

* minor

* oops, misplaced comment

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Author: kim-em

src/category_theory/limits/shapes/images.lean

@@ -126,13 +126,12 @@ def image : C := (image.mono_factorisation f).I
 def image.ι : image f ⟶ Y := (image.mono_factorisation f).m
 @[simp] lemma image.as_ι : (image.mono_factorisation f).m = image.ι f := rfl
 instance : mono (image.ι f) := (image.mono_factorisation f).m_mono
-/-- The 'corestriction' morphism from the source to the image. -/
-def image.c : X ⟶ image f := (image.mono_factorisation f).e
-@[simp] lemma image.as_c : (image.mono_factorisation f).e = image.c f := rfl
-@[simp] lemma image.c_ι : image.c f ≫ image.ι f = f := by erw (image.mono_factorisation f).fac
 
 /-- The map from the source to the image of a morphism. -/
 def factor_thru_image : X ⟶ image f := (image.mono_factorisation f).e
+/-- Rewrite in terms of the `factor_thru_image` interface. -/
+@[simp]
+lemma as_factor_thru_image : (image.mono_factorisation f).e = factor_thru_image f := rfl
 @[simp, reassoc]
 lemma image.fac : factor_thru_image f ≫ image.ι f = f := (image.mono_factorisation f).fac'