mathlib

ac01c538 - chore(data/finset/basic): Scope variables over smaller sections (#16613)

chore(data/finset/basic): Scope variables over smaller sections (#16613) Having everything in huge sections makes it harder to adjust typeclasses and variable names locally.