-- Mathlib.Order.Std
LinearOrder.OfStdArgs.mk.injEq : ∀ {α : Type u_1} (toPartialOrderArgs : PartialOrder.OfStdArgs α)
  (isLinearOrder :
    autoParam
      (let this := toPartialOrderArgs.le;
      Std.IsLinearOrder α)
      LinearOrder.OfStdArgs.isLinearOrder._autoParam)
  (decidableLE : autoParam (DecidableLE α) LinearOrder.OfStdArgs.decidableLE._autoParam)
  (decidableEq :
    autoParam
      (let this := toPartialOrderArgs;
      let this := decidableLE;
      DecidableEq α)
      LinearOrder.OfStdArgs.decidableEq._autoParam)
  (decidableLT :
    autoParam
      (let this := toPartialOrderArgs.toPreorderArgs;
      let this := decidableLE;
      DecidableLT α)
      LinearOrder.OfStdArgs.decidableLT._autoParam)
  (min :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this := decidableLE;
      Min α)
      LinearOrder.OfStdArgs.min._autoParam)
  (max :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this := decidableLE;
      Max α)
      LinearOrder.OfStdArgs.max._autoParam)
  (lawfulOrderLeftLeaningMin :
    autoParam (Std.LawfulOrderLeftLeaningMin α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMin._autoParam)
  (lawfulOrderLeftLeaningMax :
    autoParam (Std.LawfulOrderLeftLeaningMax α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMax._autoParam)
  (ord :
    autoParam
      (let this := toPartialOrderArgs.lt;
      let this := decidableEq;
      let this := decidableLT;
      Ord α)
      LinearOrder.OfStdArgs.ord._autoParam)
  (lawfulOrderOrd :
    autoParam
      (let this := toPartialOrderArgs.le;
      let this_1 := toPartialOrderArgs.lt;
      let this_2 := ⋯;
      let this_3 := isLinearOrder;
      let this_4 := decidableEq;
      let this_5 := decidableLT;
      Std.LawfulOrderOrd α)
      LinearOrder.OfStdArgs.lawfulOrderOrd._autoParam)
  (toPartialOrderArgs_1 : PartialOrder.OfStdArgs α)
  (isLinearOrder_1 :
    autoParam
      (let this := toPartialOrderArgs_1.le;
      Std.IsLinearOrder α)
      LinearOrder.OfStdArgs.isLinearOrder._autoParam)
  (decidableLE_1 : autoParam (DecidableLE α) LinearOrder.OfStdArgs.decidableLE._autoParam)
  (decidableEq_1 :
    autoParam
      (let this := toPartialOrderArgs_1;
      let this := decidableLE_1;
      DecidableEq α)
      LinearOrder.OfStdArgs.decidableEq._autoParam)
  (decidableLT_1 :
    autoParam
      (let this := toPartialOrderArgs_1.toPreorderArgs;
      let this := decidableLE_1;
      DecidableLT α)
      LinearOrder.OfStdArgs.decidableLT._autoParam)
  (min_1 :
    autoParam
      (let this := toPartialOrderArgs_1.le;
      let this := decidableLE_1;
      Min α)
      LinearOrder.OfStdArgs.min._autoParam)
  (max_1 :
    autoParam
      (let this := toPartialOrderArgs_1.le;
      let this := decidableLE_1;
      Max α)
      LinearOrder.OfStdArgs.max._autoParam)
  (lawfulOrderLeftLeaningMin_1 :
    autoParam (Std.LawfulOrderLeftLeaningMin α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMin._autoParam)
  (lawfulOrderLeftLeaningMax_1 :
    autoParam (Std.LawfulOrderLeftLeaningMax α) LinearOrder.OfStdArgs.lawfulOrderLeftLeaningMax._autoParam)
  (ord_1 :
    autoParam
      (let this := toPartialOrderArgs_1.lt;
      let this := decidableEq_1;
      let this := decidableLT_1;
      Ord α)
      LinearOrder.OfStdArgs.ord._autoParam)
  (lawfulOrderOrd_1 :
    autoParam
      (let this := toPartialOrderArgs_1.le;
      let this_1 := toPartialOrderArgs_1.lt;
      let this_2 := ⋯;
      let this_3 := isLinearOrder_1;
      let this_4 := decidableEq_1;
      let this_5 := decidableLT_1;
      Std.LawfulOrderOrd α)
      LinearOrder.OfStdArgs.lawfulOrderOrd._autoParam),
  ({ toPartialOrderArgs := toPartialOrderArgs, isLinearOrder := isLinearOrder, decidableLE := decidableLE,
        decidableEq := decidableEq, decidableLT := decidableLT, min := min, max := max,
        lawfulOrderLeftLeaningMin := lawfulOrderLeftLeaningMin, lawfulOrderLeftLeaningMax := lawfulOrderLeftLeaningMax,
        ord := ord, lawfulOrderOrd := lawfulOrderOrd } =
      { toPartialOrderArgs := toPartialOrderArgs_1, isLinearOrder := isLinearOrder_1, decidableLE := decidableLE_1,
        decidableEq := decidableEq_1, decidableLT := decidableLT_1, min := min_1, max := max_1,
        lawfulOrderLeftLeaningMin := lawfulOrderLeftLeaningMin_1,
        lawfulOrderLeftLeaningMax := lawfulOrderLeftLeaningMax_1, ord := ord_1, lawfulOrderOrd := lawfulOrderOrd_1 }) =
    (toPartialOrderArgs = toPartialOrderArgs_1 ∧
      decidableLE ≍ decidableLE_1 ∧
        decidableEq = decidableEq_1 ∧ decidableLT ≍ decidableLT_1 ∧ min = min_1 ∧ max = max_1 ∧ ord = ord_1)