case intro.intro
α : Type u
β : Type v
X : Type ?u.45555
ι : Type ?u.45558
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ (y : α), y ∈ closedBall x R → p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ (z : α), z ∈ closedBall x R → p z
⊢ p y
α : Type u
β : Type v
X : Type ?u.45555
ι : Type ?u.45558
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ (y : α), y ∈ closedBall x R → p y
y : α
⊢ p y
obtain ⟨R, hR, h⟩ : ∃ R ≥ dist y x, ∀ z : α, z ∈ closedBall x R → p z :=
  frequently_iff.1 H (Ici_mem_atTop (dist y x))
no goals
case intro.intro
α : Type u
β : Type v
X : Type ?u.45555
ι : Type ?u.45558
inst✝ : PseudoMetricSpace α
x✝ y✝ z : α
δ ε ε₁ ε₂ : ℝ
s : Set α
p : α → Prop
x : α
H : ∃ᶠ (R : ℝ) in atTop, ∀ (y : α), y ∈ closedBall x R → p y
y : α
R : ℝ
hR : R ≥ dist y x
h : ∀ (z : α), z ∈ closedBall x R → p z
⊢ p y
exact h _ hR