-- Mathlib.Order.Std
LinearOrder.OfStdArgs.mk.inj : ∀ {α : 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