Commit 2024-09-23 13:56 0c560e41

chore(Data/Finset): move non-lattice lemma out of lattice file (#17048) This lemma doesn't require finset lattice machinery to prove, and is out-of-place in its current location. Thus, we move it alongside other Finset.range lemmas. This is in part so that this lemma can be used without importing more of mathlib, and in part to help with a split of the lattice file, which would leave this particular lemma essentially homeless.