have : t ∩ Ioi x ∈ 𝓝[>] x := by
  simp only [mem_nhdsWithin]
  use t
  simp only [subset_inter_iff, inter_subset_left, inter_subset_right, and_self,
    and_true, t]
  simp
  refine ⟨?_, by simp [hu2]⟩
  simp [Metric.isOpen_iff] at hu ⊢
  intro x hx
  obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx
  simp only [Metric.ball, dist_sub_eq_dist_add_right, setOf_subset_setOf] at hε ⊢
  exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩
case intro.intro.intro
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}
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v
case intro.intro.intro
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
⊢ ∀ᶠ (x : ℝ) in 𝓝[>] x, f x + a ∈ v