Lean: 'some value occurs infinitely often' for a bounded ℕ-sequence via Finite.exists_infinite_fiber

To prove ∃ A, ∀ N, ∃ n ≥ N, a n = A from a bound a n ≤ B, map into Fin (B+1) with f n := ⟨a n, _⟩. Then Finite.exists_infinite_fiber f gives y with Infinite (f ⁻¹' {y}). Convert it with Set.infinite_coe_iff.mp and then Set.infinite_iff_exists_gt.mp _ N, which lives in Mathlib.Order.Interval.Finset.Basic; import it. Dot notation .exists_gt on a Set.Infinite value fails because the def unfolds to ¬ s.Finite. Two smaller lessons: (1) if_neg is deprecated in this Mathlib, and unfold f; split_ifs with h is the robust way to evaluate an if-defined step. (2) For an 'increase by 3 until you hit a square' argument, a strong induction on y - x was easy, with the target square y fixed in advance. Remember to also return the lower bound x ≤ s*s in the conclusion, or later case analysis is stuck.