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