feat: adds some unexpanders for functors. (#2545)

A (category-theoretic) functor is defined to extend a `Prefunctor`, which has data fields `obj` and `map`.
We routinely use `F.obj` as a spelling for `F.toPrefunctor.obj` and similarly for `map`.
However, when pretty printed, an application of this function would display as `Prefunctor.obj F.toPrefunctor X` and the analogous thing for `map`. 

This PR is an attempt to fix this with two unexpanders, one for `obj` and one for `map`.

[Zulip "discussion"](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/unexpanders.20for.20functors/near/338492828)

Mathlib/CategoryTheory/Functor/Basic.lean

@@ -54,6 +54,24 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.
 add_decl_doc Functor.toPrefunctor
 #align category_theory.functor.to_prefunctor CategoryTheory.Functor.toPrefunctor
 
+/--
+This unexpander will pretty print `F.obj X` properly.
+Without this, we would have `Prefunctor.obj F.toPrefunctor X`.
+-/
+@[app_unexpander Prefunctor.obj] def
+  unexpandFunctorObj : Lean.PrettyPrinter.Unexpander
+  | `($_ $(F).toPrefunctor $X)  => set_option hygiene false in `($(F).obj $X)
+  | _                           => throw ()
+
+/--
+This unexpander will pretty print `F.map f` properly.
+Without this, we would have `Prefunctor.map F.toPrefunctor f`.
+-/
+@[app_unexpander Prefunctor.map] def
+  unexpandFunctorMap : Lean.PrettyPrinter.Unexpander
+  | `($_ $(F).toPrefunctor $X)  => set_option hygiene false in `($(F).map $X)
+  | _                           => throw ()
+
 end
 
 /-- Notation for a functor between categories. -/