refactor(data/finset/basic): simplify proof (#6160)
... of `bUnion_filter_eq_of_maps_to`
looks nicer, slightly faster elaboration, 13% smaller proof term
Co-authors: `lean-gptf`, Stanislas Polu
Co-authored-by: Jesse Michael Han <39395247+jesse-michael-han@users.noreply.github.com>
