{α : Type u} →
  {P : Sort u_1} →
    {toLinearPreorderOfLEArgs : Std.Packages.LinearPreorderOfLEArgs α} →
      {le_antisymm :
          autoParam
            (let this := toLinearPreorderOfLEArgs.le;
            ∀ (a b : α), a ≤ b → b ≤ a → a = b)
            Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam} →
        {min :
            autoParam
              (let this := toLinearPreorderOfLEArgs.le;
              let this := toLinearPreorderOfLEArgs.decidableLE;
              Min α)
              Std.Packages.LinearOrderOfLEArgs.min._autoParam} →
          {max :
              autoParam
                (let this := toLinearPreorderOfLEArgs.le;
                let this := toLinearPreorderOfLEArgs.decidableLE;
                Max α)
                Std.Packages.LinearOrderOfLEArgs.max._autoParam} →
            {min_eq :
                autoParam
                  (let this := toLinearPreorderOfLEArgs.le;
                  let this_1 := toLinearPreorderOfLEArgs.decidableLE;
                  let this_2 := min;
                  ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
                  Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam} →
              {max_eq :
                  autoParam
                    (let this := toLinearPreorderOfLEArgs.le;
                    let this_1 := toLinearPreorderOfLEArgs.decidableLE;
                    let this_2 := max;
                    ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
                    Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam} →
                {toLinearPreorderOfLEArgs' : Std.Packages.LinearPreorderOfLEArgs α} →
                  {le_antisymm' :
                      autoParam
                        (let this := toLinearPreorderOfLEArgs'.le;
                        ∀ (a b : α), a ≤ b → b ≤ a → a = b)
                        Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam} →
                    {min' :
                        autoParam
                          (let this := toLinearPreorderOfLEArgs'.le;
                          let this := toLinearPreorderOfLEArgs'.decidableLE;
                          Min α)
                          Std.Packages.LinearOrderOfLEArgs.min._autoParam} →
                      {max' :
                          autoParam
                            (let this := toLinearPreorderOfLEArgs'.le;
                            let this := toLinearPreorderOfLEArgs'.decidableLE;
                            Max α)
                            Std.Packages.LinearOrderOfLEArgs.max._autoParam} →
                        {min_eq' :
                            autoParam
                              (let this := toLinearPreorderOfLEArgs'.le;
                              let this_1 := toLinearPreorderOfLEArgs'.decidableLE;
                              let this_2 := min';
                              ∀ (a b : α), a ⊓ b = if a ≤ b then a else b)
                              Std.Packages.LinearOrderOfLEArgs.min_eq._autoParam} →
                          {max_eq' :
                              autoParam
                                (let this := toLinearPreorderOfLEArgs'.le;
                                let this_1 := toLinearPreorderOfLEArgs'.decidableLE;
                                let this_2 := max';
                                ∀ (a b : α), a ⊔ b = if b ≤ a then a else b)
                                Std.Packages.LinearOrderOfLEArgs.max_eq._autoParam} →
                            { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs, le_antisymm := le_antisymm,
                                  min := min, max := max, min_eq := min_eq, max_eq := max_eq } =
                                { toLinearPreorderOfLEArgs := toLinearPreorderOfLEArgs', le_antisymm := le_antisymm',
                                  min := min', max := max', min_eq := min_eq', max_eq := max_eq' } →
                              (toLinearPreorderOfLEArgs ≍ toLinearPreorderOfLEArgs' → min ≍ min' → max ≍ max' → P) → P