Commit 2021-11-29 17:49 bc4ed5c0

chore(*): cleanup unneeded uses of by_cases across the library (#10523) Many proofs in the library do case splits but then never use the introduced assumption in one of the cases, meaning the case split can be removed and replaced with the general argument. Its easy to either accidentally introduce these more complicated than needed arguments when writing proofs, or in some cases presumably refactors made assumptions unnecessary, we golf / simplify several of these to simplify these proofs. Similar things happen for split_ifs and explicit if ... then proofs. Rather remarkably the changes to uniformly_extend_spec make the separated space assumption unnecessary too, and removing this removes this assumption from around 10 other lemmas in the library too. Some more random golfs were added in the review process Found with a work in progress linter.