-- Init.Data.Order.PackageFactories
Std.Packages.PreorderOfLEArgs.mk.inj : ∀ {α : Type u} {le : autoParam (LE α) Std.Packages.PreorderOfLEArgs.le._autoParam}
  {decidableLE : autoParam (DecidableLE α) Std.Packages.PreorderOfLEArgs.decidableLE._autoParam}
  {lt :
    autoParam
      (let this := le;
      LT α)
      Std.Packages.PreorderOfLEArgs.lt._autoParam}
  {beq :
    autoParam
      (let this := le;
      let this := decidableLE;
      BEq α)
      Std.Packages.PreorderOfLEArgs.beq._autoParam}
  {lt_iff :
    autoParam
      (let this := le;
      let this_1 := lt;
      ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)
      Std.Packages.PreorderOfLEArgs.lt_iff._autoParam}
  {decidableLT :
    autoParam
      (let this := le;
      let this := decidableLE;
      let this := lt;
      have this_1 := lt_iff;
      DecidableLT α)
      Std.Packages.PreorderOfLEArgs.decidableLT._autoParam}
  {beq_iff_le_and_ge :
    autoParam
      (let this := le;
      let this_1 := decidableLE;
      let this_2 := beq;
      ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a)
      Std.Packages.PreorderOfLEArgs.beq_iff_le_and_ge._autoParam}
  {le_refl :
    autoParam
      (let this := le;
      ∀ (a : α), a ≤ a)
      Std.Packages.PreorderOfLEArgs.le_refl._autoParam}
  {le_trans :
    autoParam
      (let this := le;
      ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
      Std.Packages.PreorderOfLEArgs.le_trans._autoParam}
  {le_1 : autoParam (LE α) Std.Packages.PreorderOfLEArgs.le._autoParam}
  {decidableLE_1 : autoParam (DecidableLE α) Std.Packages.PreorderOfLEArgs.decidableLE._autoParam}
  {lt_1 :
    autoParam
      (let this := le_1;
      LT α)
      Std.Packages.PreorderOfLEArgs.lt._autoParam}
  {beq_1 :
    autoParam
      (let this := le_1;
      let this := decidableLE_1;
      BEq α)
      Std.Packages.PreorderOfLEArgs.beq._autoParam}
  {lt_iff_1 :
    autoParam
      (let this := le_1;
      let this_1 := lt_1;
      ∀ (a b : α), a < b ↔ a ≤ b ∧ ¬b ≤ a)
      Std.Packages.PreorderOfLEArgs.lt_iff._autoParam}
  {decidableLT_1 :
    autoParam
      (let this := le_1;
      let this := decidableLE_1;
      let this := lt_1;
      have this_1 := lt_iff_1;
      DecidableLT α)
      Std.Packages.PreorderOfLEArgs.decidableLT._autoParam}
  {beq_iff_le_and_ge_1 :
    autoParam
      (let this := le_1;
      let this_1 := decidableLE_1;
      let this_2 := beq_1;
      ∀ (a b : α), (a == b) = true ↔ a ≤ b ∧ b ≤ a)
      Std.Packages.PreorderOfLEArgs.beq_iff_le_and_ge._autoParam}
  {le_refl_1 :
    autoParam
      (let this := le_1;
      ∀ (a : α), a ≤ a)
      Std.Packages.PreorderOfLEArgs.le_refl._autoParam}
  {le_trans_1 :
    autoParam
      (let this := le_1;
      ∀ (a b c : α), a ≤ b → b ≤ c → a ≤ c)
      Std.Packages.PreorderOfLEArgs.le_trans._autoParam},
  { le := le, decidableLE := decidableLE, lt := lt, beq := beq, lt_iff := lt_iff, decidableLT := decidableLT,
        beq_iff_le_and_ge := beq_iff_le_and_ge, le_refl := le_refl, le_trans := le_trans } =
      { le := le_1, decidableLE := decidableLE_1, lt := lt_1, beq := beq_1, lt_iff := lt_iff_1,
        decidableLT := decidableLT_1, beq_iff_le_and_ge := beq_iff_le_and_ge_1, le_refl := le_refl_1,
        le_trans := le_trans_1 } →
    le = le_1 ∧ decidableLE ≍ decidableLE_1 ∧ lt = lt_1 ∧ beq = beq_1 ∧ decidableLT ≍ decidableLT_1