mathlib

89697a24 - feat(data/fintype/order): complete order instances for fintype (#7123)

feat(data/fintype/order): complete order instances for fintype (#7123) This PR adds several instances (as defs) for fintypes: * `order_bot` from `semilattice_inf`, `order_top` from `semilattice_sup`, `bounded_order` from `lattice`. * `complete_lattice` from `lattice`. * `complete_linear_order` from `linear_order`. We use this last one to give a `complete_linear_order` instance for `fin (n + 1)` . Co-authored-by: Peter Nelson <apnelson@uwaterloo.ca> Co-authored-by: Peter Nelson <71660771+apnelson1@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: YaelDillies <yael.dillies@gmail.com>