{α : Type u_5} →
  {P : Sort u} →
    {toField : Field α} →
      {toConditionallyCompleteLinearOrder : ConditionallyCompleteLinearOrder α} →
        {toIsOrderedCancelAddMonoid : IsOrderedCancelAddMonoid α} →
          {toZeroLEOneClass : ZeroLEOneClass α} →
            {toPosMulStrictMono : PosMulStrictMono α} →
              {toMulPosStrictMono : MulPosStrictMono α} →
                {toField' : Field α} →
                  {toConditionallyCompleteLinearOrder' : ConditionallyCompleteLinearOrder α} →
                    {toIsOrderedCancelAddMonoid' : IsOrderedCancelAddMonoid α} →
                      {toZeroLEOneClass' : ZeroLEOneClass α} →
                        {toPosMulStrictMono' : PosMulStrictMono α} →
                          {toMulPosStrictMono' : MulPosStrictMono α} →
                            { toField := toField,
                                  toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder,
                                  toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid,
                                  toZeroLEOneClass := toZeroLEOneClass, toPosMulStrictMono := toPosMulStrictMono,
                                  toMulPosStrictMono := toMulPosStrictMono } =
                                { toField := toField',
                                  toConditionallyCompleteLinearOrder := toConditionallyCompleteLinearOrder',
                                  toIsOrderedCancelAddMonoid := toIsOrderedCancelAddMonoid',
                                  toZeroLEOneClass := toZeroLEOneClass', toPosMulStrictMono := toPosMulStrictMono',
                                  toMulPosStrictMono := toMulPosStrictMono' } →
                              (toField ≍ toField' →
                                  toConditionallyCompleteLinearOrder ≍ toConditionallyCompleteLinearOrder' → P) →
                                P