mathlib3

de6f57d2 - chore(ring_theory/unique_factorization_domain): Eliminate `finish` (#11055)

chore(ring_theory/unique_factorization_domain): Eliminate `finish` (#11055) Removing uses of finish, as discussed in this Zulip thread (https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/mathlib.20sat.20solvers)