chore: fix typo (#21043)

Co-authored-by: Markus Himmel <markus@lean-fro.org>

Author: TwoFX

Mathlib/CategoryTheory/Limits/Shapes/Images.lean

@@ -24,7 +24,7 @@ so that `m` factors through the `m'` in any other such factorisation.
     morphism `e`.
 * `HasImages C` means that every morphism in `C` has an image.
 * Let `f : X ⟶ Y` and `g : P ⟶ Q` be morphisms in `C`, which we will represent as objects of the
-  arrow category `arrow C`. Then `sq : f ⟶ g` is a commutative square in `C`. If `f` and `g` have
+  arrow category `Arrow C`. Then `sq : f ⟶ g` is a commutative square in `C`. If `f` and `g` have
   images, then `HasImageMap sq` represents the fact that there is a morphism
   `i : image f ⟶ image g` making the diagram
 
@@ -241,7 +241,7 @@ def ofArrowIso {f g : Arrow C} (F : ImageFactorisation f.hom) (sq : f ⟶ g) [Is
 
 end ImageFactorisation
 
-/-- `has_image f` means that there exists an image factorisation of `f`. -/
+/-- `HasImage f` means that there exists an image factorisation of `f`. -/
 class HasImage (f : X ⟶ Y) : Prop where mk' ::
   exists_image : Nonempty (ImageFactorisation f)
 

Mathlib/CategoryTheory/Monoidal/Functor.lean

@@ -55,7 +55,7 @@ namespace Functor
 -- "weigh more" than structural maps.
 -- (However by this argument `associativity` is currently stated backwards!)
 /-- A functor `F : C ⥤ D` between monoidal categories is lax monoidal if it is
-equipped with morphisms `ε : 𝟙 _D ⟶ F.obj (𝟙_ C)` and `μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)`,
+equipped with morphisms `ε : 𝟙_ D ⟶ F.obj (𝟙_ C)` and `μ X Y : F.obj X ⊗ F.obj Y ⟶ F.obj (X ⊗ Y)`,
 satisfying the appropriate coherences. -/
 class LaxMonoidal where
   /-- unit morphism -/