feat(category_theory): cancel fully faithful functor (#3920)
feat(category_theory): cancel fully faithful functor (#3920)

Construct the natural isomorphism between `F` and `G` given a natural iso between `F ⋙ H` and `G ⋙ H` for a fully faithful `H`. 

Co-authored-by: Thomas Read <4685143895332bfc258c419e966bdaff0e6ba217@gmail.com>



leanprover-community/mathlib,leanprover-community/mathlib