Frequently in finite set

theorem frequently_in_finite_set {X : Type*} [Finite X] {s : Set X} {xs : Stream' X} :    (∃ᶠ 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 [rf, Set.range, ← Nat.frequently_atTop_iff_infinite] at h_inf'    use x ; simp [h_x]    apply Frequently.mono h_inf'    tauto  · rintro ⟨x, h_x, h_inf⟩    apply Frequently.mono h_inf    intro k h_k ; simpa [h_k]