-- Init.Data.Order.PackageFactories
Std.Packages.LinearPreorderOfOrdArgs.mk.injEq : ∀ {α : 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)