Commit 2024-08-01 00:14 a904cfd0

chore: backports for leanprover/lean4#4814 (part 1) (#15245) The new variables inclusion mechanism https://github.com/leanprover/lean4/pull/4814 is going to require many changes to Mathlib. Some of these changes are to make sure typeclass hypotheses are not unnecessarily included. This is achieved either by using section to bound variable [...], using variable ... in, or reordering theorems. (I think you can see all three being using here.) Other changes require adding include ... to include variables that the new mechanism won't automatically include. These changes can't be backported to master, and instead are accumulating on the lean-pr-testing-4814 branch.