∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  NumberField.house.supOfBasis✝ K =
    Finset.univ.sup' ⋯ fun r =>
      NumberField.house ((algebraMap (NumberField.RingOfIntegers K) K) ((NumberField.house.newBasis✝ K) r))