Tendsto_nhdsWithin_punctured_map_add

lemma Tendsto_nhdsWithin_punctured_map_add {f : ℝ → ℝ} (a x : ℝ)    (f_mono : StrictMono f) (f_iso : Isometry f) :    Tendsto (fun y ↦ f y + a) (𝓝[>] x) (𝓝[>] (f x + a)) := by  refine tendsto_iff_forall_eventually_mem.mpr ?_  intro v hv  simp only [mem_nhdsWithin] at hv  obtain ⟨u, hu, hu2, hu3⟩ := hv  let t := {x | f x + a ∈ u}  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, mem_setOf_eq]    refine ⟨?_, by simp [hu2]⟩    simp only [Metric.isOpen_iff, gt_iff_lt, mem_setOf_eq] at hu ⊢    intro x hx    obtain ⟨ε, εpos, hε⟩ := hu (f x + a) hx    simp only [Metric.ball, setOf_subset_setOf] at hε ⊢    exact ⟨ε, εpos, fun _ hy ↦ hε (by simp [isometry_iff_dist_eq.mp f_iso, hy])⟩  filter_upwards [this]  intro b hb  simp only [mem_inter_iff, mem_setOf_eq, mem_Ioi, t] at hb  refine hu3 ?_  simp only [mem_inter_iff, mem_Ioi, add_lt_add_iff_right]  exact ⟨hb.1, f_mono hb.2⟩