mathlib

e8339bd6 - feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327)

feat(category_theory/fully_faithful): nat_trans_of_comp_fully_faithful (#13327) I added `nat_iso_of_comp_fully_faithful` in an earlier PR, but left out the more basic construction. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>