Frequently in finite type

theorem frequently_in_finite_type [Finite α] {s : Set α} {xs : ωSequence α} :    (∃ᶠ k in atTop, xs k ∈ s) ↔ ∃ x ∈ s, ∃ᶠ k in atTop, xs k = x := by  constructor  · intro h_inf    rw [Nat.frequently_atTop_iff_infinite] at h_inf    have : Infinite (xs ⁻¹' s) := h_inf.to_subtype    let rf := Set.restrictPreimage s xs    obtain ⟨⟨x, h_x⟩, h_inf'⟩ := Finite.exists_infinite_fiber rf    rw [← Set.infinite_range_iff (Subtype.val_injective.comp Subtype.val_injective)] at h_inf'    simp only [range, comp_apply, Subtype.exists, mem_preimage, mem_singleton_iff,      restrictPreimage_mk, Subtype.mk.injEq, ← Nat.frequently_atTop_iff_infinite, rf] at h_inf'    grind  · rintro ⟨_, _, h_inf⟩    apply Frequently.mono h_inf    grind