mathlib

f525f93e - chore(*): Eliminate `finish` (#10970)

chore(*): Eliminate `finish` (#10970) Eliminating the use of `finish` in `data/set/basic`, `order/filter/bases`, and `topology/algebra/valued_field`.