mathlib3

d1ba87a9 - feat(category_theory/faithful): faithful.of_iso (#2453)

feat(category_theory/faithful): faithful.of_iso (#2453) A minor useful lemma, about to be abandoned on another branch. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>