mathlib3

dc093e91 - chore(combinatorics/configuration): don't use classical.some in a proof (#12515)