simp_rw [hp.mem_iff, ← exists_prop, mem_inter_iff, mem_closedBall_zero_iff]
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ (∃ i, ∃ (_ : 0 < i), φ i ⊆ s) ↔ ∃ i, ∃ (_ : 0 < i), ∀ ⦃x : ℝ⦄, ‖x‖ ≤ i ∧ x ∈ Ioi 0 → φ x ⊆ s