-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.mk.inj : ∀ {α : Type u} {ord : autoParam (Ord α) Std.Packages.LinearPreorderOfOrdArgs.ord._autoParam}
  {transOrd : autoParam (Std.TransOrd α) Std.Packages.LinearPreorderOfOrdArgs.transOrd._autoParam}
  {le :
    autoParam
      (let this := ord;
      LE α)
      Std.Packages.LinearPreorderOfOrdArgs.le._autoParam}
  {lawfulOrderOrd :
    autoParam
      (let this := ord;
      let this_1 := transOrd;
      let this_2 := le;
      Std.LawfulOrderOrd α)
      Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd._autoParam}
  {decidableLE :
    autoParam
      (let this := ord;
      let this := le;
      have this_1 := lawfulOrderOrd;
      DecidableLE α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLE._autoParam}
  {lt :
    autoParam
      (let this := ord;
      LT α)
      Std.Packages.LinearPreorderOfOrdArgs.lt._autoParam}
  {lt_iff :
    autoParam
      (let this := ord;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      let this_3 := lt;
      ∀ (a b : α), a < b ↔ compare a b = Ordering.lt)
      Std.Packages.LinearPreorderOfOrdArgs.lt_iff._autoParam}
  {decidableLT :
    autoParam
      (let this := ord;
      let this := lt;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      have this_3 := lt_iff;
      DecidableLT α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLT._autoParam}
  {beq :
    autoParam
      (let this := ord;
      BEq α)
      Std.Packages.LinearPreorderOfOrdArgs.beq._autoParam}
  {beq_iff :
    autoParam
      (let this := ord;
      let this_1 := le;
      have this_2 := lawfulOrderOrd;
      let this_3 := beq;
      ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq)
      Std.Packages.LinearPreorderOfOrdArgs.beq_iff._autoParam}
  {ord_1 : autoParam (Ord α) Std.Packages.LinearPreorderOfOrdArgs.ord._autoParam}
  {transOrd_1 : autoParam (Std.TransOrd α) Std.Packages.LinearPreorderOfOrdArgs.transOrd._autoParam}
  {le_1 :
    autoParam
      (let this := ord_1;
      LE α)
      Std.Packages.LinearPreorderOfOrdArgs.le._autoParam}
  {lawfulOrderOrd_1 :
    autoParam
      (let this := ord_1;
      let this_1 := transOrd_1;
      let this_2 := le_1;
      Std.LawfulOrderOrd α)
      Std.Packages.LinearPreorderOfOrdArgs.lawfulOrderOrd._autoParam}
  {decidableLE_1 :
    autoParam
      (let this := ord_1;
      let this := le_1;
      have this_1 := lawfulOrderOrd_1;
      DecidableLE α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLE._autoParam}
  {lt_1 :
    autoParam
      (let this := ord_1;
      LT α)
      Std.Packages.LinearPreorderOfOrdArgs.lt._autoParam}
  {lt_iff_1 :
    autoParam
      (let this := ord_1;
      let this_1 := le_1;
      have this_2 := lawfulOrderOrd_1;
      let this_3 := lt_1;
      ∀ (a b : α), a < b ↔ compare a b = Ordering.lt)
      Std.Packages.LinearPreorderOfOrdArgs.lt_iff._autoParam}
  {decidableLT_1 :
    autoParam
      (let this := ord_1;
      let this := lt_1;
      let this_1 := le_1;
      have this_2 := lawfulOrderOrd_1;
      have this_3 := lt_iff_1;
      DecidableLT α)
      Std.Packages.LinearPreorderOfOrdArgs.decidableLT._autoParam}
  {beq_1 :
    autoParam
      (let this := ord_1;
      BEq α)
      Std.Packages.LinearPreorderOfOrdArgs.beq._autoParam}
  {beq_iff_1 :
    autoParam
      (let this := ord_1;
      let this_1 := le_1;
      have this_2 := lawfulOrderOrd_1;
      let this_3 := beq_1;
      ∀ (a b : α), (a == b) = true ↔ compare a b = Ordering.eq)
      Std.Packages.LinearPreorderOfOrdArgs.beq_iff._autoParam},
  { ord := ord, transOrd := transOrd, le := le, lawfulOrderOrd := lawfulOrderOrd, decidableLE := decidableLE, lt := lt,
        lt_iff := lt_iff, decidableLT := decidableLT, beq := beq, beq_iff := beq_iff } =
      { ord := ord_1, transOrd := transOrd_1, le := le_1, lawfulOrderOrd := lawfulOrderOrd_1,
        decidableLE := decidableLE_1, lt := lt_1, lt_iff := lt_iff_1, decidableLT := decidableLT_1, beq := beq_1,
        beq_iff := beq_iff_1 } →
    ord = ord_1 ∧ le = le_1 ∧ decidableLE ≍ decidableLE_1 ∧ lt = lt_1 ∧ decidableLT ≍ decidableLT_1 ∧ beq = beq_1