mathlib3

96d748eb - refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893)

refactor(category_theory): rename `functor.on_iso` to `functor.map_iso` (#893) * feat(category_theory): functor.map_nat_iso * define `functor.map_nat_iso`, and relate to whiskering * rename `functor.on_iso` to `functor.map_iso` * add some missing lemmas about whiskering * some more missing whiskering lemmas, while we're at it * removing map_nat_iso