mathlib3

e104992d - chore(order/*): Replace total partial orders by linear orders (#13839)

chore(order/*): Replace total partial orders by linear orders (#13839) `partial_order α` + `is_total α (≤)` has no more theorems than `linear_order α` but is nonetheless used in some places. This replaces those uses by `linear_order α` or `complete_linear_order α`. Also make implicit one argument of `finset.lt_inf'_iff` and friends.