{α : Type u} →
  {P : Sort u_1} →
    {toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α} →
      {ord :
          autoParam
            (let this := toPreorderOfLEArgs.le;
            let this := toPreorderOfLEArgs.decidableLE;
            Ord α)
            Std.Packages.LinearPreorderOfLEArgs.ord._autoParam} →
        {le_total : autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam} →
          {isLE_compare :
              autoParam
                (let this := toPreorderOfLEArgs.le;
                let this_1 := toPreorderOfLEArgs.decidableLE;
                let this_2 := ord;
                ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
                Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam} →
            {isGE_compare :
                autoParam
                  (let this := toPreorderOfLEArgs.le;
                  let this_1 := toPreorderOfLEArgs.decidableLE;
                  have this_2 := le_total;
                  let this_3 := ord;
                  ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
                  Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam} →
              {toPreorderOfLEArgs' : Std.Packages.PreorderOfLEArgs α} →
                {ord' :
                    autoParam
                      (let this := toPreorderOfLEArgs'.le;
                      let this := toPreorderOfLEArgs'.decidableLE;
                      Ord α)
                      Std.Packages.LinearPreorderOfLEArgs.ord._autoParam} →
                  {le_total' :
                      autoParam (∀ (a b : α), a ≤ b ∨ b ≤ a) Std.Packages.LinearPreorderOfLEArgs.le_total._autoParam} →
                    {isLE_compare' :
                        autoParam
                          (let this := toPreorderOfLEArgs'.le;
                          let this_1 := toPreorderOfLEArgs'.decidableLE;
                          let this_2 := ord';
                          ∀ (a b : α), (compare a b).isLE = true ↔ a ≤ b)
                          Std.Packages.LinearPreorderOfLEArgs.isLE_compare._autoParam} →
                      {isGE_compare' :
                          autoParam
                            (let this := toPreorderOfLEArgs'.le;
                            let this_1 := toPreorderOfLEArgs'.decidableLE;
                            have this_2 := le_total';
                            let this_3 := ord';
                            ∀ (a b : α), (compare a b).isGE = true ↔ b ≤ a)
                            Std.Packages.LinearPreorderOfLEArgs.isGE_compare._autoParam} →
                        { toPreorderOfLEArgs := toPreorderOfLEArgs, ord := ord, le_total := le_total,
                              isLE_compare := isLE_compare, isGE_compare := isGE_compare } =
                            { toPreorderOfLEArgs := toPreorderOfLEArgs', ord := ord', le_total := le_total',
                              isLE_compare := isLE_compare', isGE_compare := isGE_compare' } →
                          (toPreorderOfLEArgs ≍ toPreorderOfLEArgs' → ord ≍ ord' → P) → P