{α : Type u_2} →
  (le lt : α → α → Prop) →
    (∀ (a : α), le a a) →
      (∀ (a b c : α), le a b → le b c → le a c) →
        autoParam (∀ (a b : α), lt a b ↔ le a b ∧ ¬le b a) Preorder.lt_iff_le_not_ge._autoParam →
          (∀ (a b : α), le a b → le b a → a = b) →
            (min max : α → α → α) →
              (compare : α → α → Ordering) →
                (∀ (a b : α), le a b ∨ le b a) →
                  (toDecidableLE : DecidableLE α) →
                    (toDecidableEq : DecidableEq α) →
                      (toDecidableLT : DecidableLT α) →
                        autoParam (∀ (a b : α), min a b = if le a b then a else b) LinearOrder.min_def._autoParam →
                          autoParam (∀ (a b : α), max a b = if le a b then b else a) LinearOrder.max_def._autoParam →
                            autoParam (∀ (a b : α), compare a b = compareOfLessAndEq a b)
                                LinearOrder.compare_eq_compareOfLessAndEq._autoParam →
                              LinearOrder α