uniform_continuity_shift

theorem uniform_continuity_shift {f : ℝ → ℝ} (a b : ℝ) (hab : a ≤ b)    (hf_cont : ∀ x ∈ Set.Icc a b, ContinuousAt f x) :    ∀ ε > 0, ∃ δ > 0, ∀ x ∈ Set.Icc a b, ∀ t, |t| < δ → |f (x - t) - f x| < ε := by      intro ε hε      by_contra h_contra;      -- By contradiction, assume there exist sequences $x_n \in [a, b]$ and $t_n$ such that $|t_n| < 1/n$ but $|f(x_n - t_n) - f(x_n)| \geq \varepsilon$.      obtain ⟨xn, t_n, hxn_bounds, ht_n_abs, h_diff⟩ : ∃ xn : ℕ → ℝ, ∃ t_n : ℕ → ℝ, (∀ n, xn n ∈ Set.Icc a b) ∧ (∀ n, abs (t_n n) < 1 / (n + 1)) ∧ (∀ n, abs (f (xn n - t_n n) - f (xn n)) ≥ ε) := by        push_neg at h_contra;        exact ⟨ fun n => Classical.choose ( h_contra ( 1 / ( n + 1 ) ) ( by positivity ) ), fun n => Classical.choose_spec ( h_contra ( 1 / ( n + 1 ) ) ( by positivity ) ) |>.2.choose, fun n => Classical.choose_spec ( h_contra ( 1 / ( n + 1 ) ) ( by positivity ) ) |>.1, fun n => Classical.choose_spec ( h_contra ( 1 / ( n + 1 ) ) ( by positivity ) ) |>.2.choose_spec.1, fun n => Classical.choose_spec ( h_contra ( 1 / ( n + 1 ) ) ( by positivity ) ) |>.2.choose_spec.2 ⟩;      -- Since $[a, b]$ is compact, there exists a convergent subsequence $x_{n_k}$ converging to some $x_0 \in [a, b]$.      obtain ⟨x₀, hx₀⟩ : ∃ x₀ ∈ Set.Icc a b, ∃ (nk : ℕ → ℕ), StrictMono nk ∧ Filter.Tendsto (fun k => xn (nk k)) Filter.atTop (nhds x₀) := by        have h_compact : IsCompact (Set.Icc a b) := by          exact CompactIccSpace.isCompact_Icc;        have := h_compact.isSeqCompact fun n => hxn_bounds n; aesop;      -- Then $t_{n_k} \to 0$, so $x_{n_k} - t_{n_k} \to x_0$.      obtain ⟨nk, hnk_mono, hnk_conv⟩ := hx₀.right      have ht_nk_zero : Filter.Tendsto (fun k => t_n (nk k)) Filter.atTop (nhds 0) := by        exact squeeze_zero_norm ( fun k => le_of_lt ( ht_n_abs _ ) ) ( tendsto_one_div_add_atTop_nhds_zero_nat.comp hnk_mono.tendsto_atTop );      have h_cont : Filter.Tendsto (fun k => f (xn (nk k) - t_n (nk k))) Filter.atTop (nhds (f x₀)) ∧ Filter.Tendsto (fun k => f (xn (nk k))) Filter.atTop (nhds (f x₀)) := by        exact ⟨ hf_cont x₀ hx₀.1 |> fun h => h.tendsto.comp <| by simpa using hnk_conv.sub ht_nk_zero, hf_cont x₀ hx₀.1 |> fun h => h.tendsto.comp <| by simpa using hnk_conv ⟩;      exact absurd ( le_of_tendsto_of_tendsto' tendsto_const_nhds ( Filter.Tendsto.abs ( h_cont.1.sub h_cont.2 ) ) fun k => h_diff ( nk k ) ) ( by norm_num; linarith )