obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
case h
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}
case h.intro.intro
f : ℝ → ℝ
a x✝ : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu2 : f x✝ + a ∈ u
hu3 : u ∩ Ioi (f x✝ + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
hu : ∀ x ∈ u, ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ u
x : ℝ
hx : f x + a ∈ u
ε : ℝ
εpos : 0 < ε
hε : Metric.ball (f x + a) ε ⊆ u
⊢ ∃ ε, 0 < ε ∧ Metric.ball x ε ⊆ {x | f x + a ∈ u}