Commit 2020-11-03 15:50 63d109fe
View on Github →chore(category_theory/limits): Use lim_map over lim.map (#4856)
Modify the simp-normal form for lim.map to be lim_map instead, and express lemmas in terms of lim_map instead, as well as use it in special shapes so that the assumptions can be weakened.