Theorem: Filter.Eventually.exists' (RMT4/hurwitz.lean)

State before:
ι : Type u_1
F : ι → ℂ → ℂ
f : ℂ → ℂ
z₀ : ℂ
p : Filter ι
r : ℝ
U : Set ℂ
P : ℝ → Prop
t₀ : ℝ
h : ∀ᶠ (t : ℝ) in 𝓝[>] t₀, P t
⊢ ∃ t > t₀, P t
Tactic:
simpa [and_comm, exists_prop] using (frequently_nhdsWithin_iff.mp h.frequently).exists
State after:
no goals