mathlib

17a33f0d - refactor(order/copy): move complete_lattice.copy to its own file (#2050)

refactor(order/copy): move complete_lattice.copy to its own file (#2050) * refactor(order/copy): move complete_lattice.copy to its own file * Docstrings * Update src/order/copy.lean Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>