Commit 2022-12-20 05:52 bf9d2899

feat: port CategoryTheory.Functor.FullyFaithful (#846) mathlib SHA: 70d50ecfd4900dd6d328da39ab7ebd516abe4025 Porting notes:

1. aesop_cat was unable to close goals that tidy was able to. I left an example proof of what tidy emits (with some cleanup).
2. unfold_projs is not ported. Is it an easy tactic to port over or is there a better "lean4" way? (ed: not needed)
3. trans doesn't seem to work with HEq (see https://github.com/leanprover-community/mathlib4/issues/1119)
4. Some documentation is needed for Full and Faithful. Please feel free to fill it in if you wish.