mathlib3

ef11fb3d - feat(category_theory/limits/opposites): (co)limits in opposite categories (#926)

feat(category_theory/limits/opposites): (co)limits in opposite categories (#926) * (co)limits in opposite categories * moving lemmas * moving stuff about complete lattices to separate PR * renaming category_of_preorder elsewhere * build limits functor/shape at a time * removing stray commas, and making one-liners * remove non-terminal simps