simp only [mem_inter_iff, mem_Ioi, add_lt_add_iff_right]
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∩ Ioi (f x + a)
case h
f : ℝ → ℝ
a x : ℝ
f_mono : StrictMono f
f_iso : Isometry f
v u : Set ℝ
hu : IsOpen u
hu2 : f x + a ∈ u
hu3 : u ∩ Ioi (f x + a) ⊆ v
t : Set ℝ := {x | f x + a ∈ u}
this : t ∩ Ioi x ∈ 𝓝[>] x
b : ℝ
hb : f b + a ∈ u ∧ x < b
⊢ f b + a ∈ u ∧ f x < f b