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.

Mathlib/Data/Finset/Basic.lean

@@ -2597,6 +2597,10 @@ lemma range_nontrivial {n : ℕ} (hn : 1 < n) : (Finset.range n).Nontrivial := b
   rw [Finset.Nontrivial, Finset.coe_range]
   exact ⟨0, Nat.zero_lt_one.trans hn, 1, hn, Nat.zero_ne_one⟩
 
+theorem exists_nat_subset_range (s : Finset ℕ) : ∃ n : ℕ, s ⊆ range n :=
+  s.induction_on (by simp)
+    fun a s _ ⟨n, hn⟩ => ⟨max (a + 1) n, insert_subset (by simp) (hn.trans (by simp))⟩
+
 end Range
 
 -- useful rules for calculations with quantifiers

Mathlib/Data/Finset/Lattice.lean

@@ -204,9 +204,6 @@ theorem _root_.List.foldr_sup_eq_sup_toFinset [DecidableEq α] (l : List α) :
 theorem subset_range_sup_succ (s : Finset ℕ) : s ⊆ range (s.sup id).succ := fun _ hn =>
   mem_range.2 <| Nat.lt_succ_of_le <| @le_sup _ _ _ _ _ id _ hn
 
-theorem exists_nat_subset_range (s : Finset ℕ) : ∃ n : ℕ, s ⊆ range n :=
-  ⟨_, s.subset_range_sup_succ⟩
-
 theorem sup_induction {p : α → Prop} (hb : p ⊥) (hp : ∀ a₁, p a₁ → ∀ a₂, p a₂ → p (a₁ ⊔ a₂))
     (hs : ∀ b ∈ s, p (f b)) : p (s.sup f) := by
   induction s using Finset.cons_induction with