mathlib

6155d435 - feat(*): rsuffices golfs (#16159)

feat(*): rsuffices golfs (#16159) This PR golfs many uses of `suffices` + `obtain`. There is further golfs possible, but I kept a specific type of golf to this PR. Most of these at least drop a line, if not two.