Function.Periodic.uniformContinuous_of_continuous

lemma Function.Periodic.uniformContinuous_of_continuous {f : ℝ → ℂ} {T : ℝ} (hT : 0 < T)    (hp : Function.Periodic f T) (hc : ContinuousOn f (Set.Icc (-T) (2 * T))) :    UniformContinuous f := by  have : IsCompact (Set.Icc (-T) (2 * T)) := isCompact_Icc  have unicont_on_Icc := this.uniformContinuousOn_of_continuous hc  rw [Metric.uniformContinuousOn_iff] at unicont_on_Icc  rw [Metric.uniformContinuous_iff]  intro ε εpos  rcases (unicont_on_Icc ε εpos) with ⟨δ, δpos, h⟩  use min δ T, lt_min δpos hT  have h1 : min δ T ≤ T := min_le_right ..  intro x y hxy  rcases (hp.exists_mem_Ico₀' hT x) with ⟨n, ha, hxa⟩  have hyb: f y = f (y - n • T) := (hp.sub_zsmul_eq n).symm  rw [hxa, hyb]  apply h (x - n • T) _ (y - n • T)  on_goal 1 => rw [dist_eq, abs_lt] at hxy  constructor <;> linarith [ha.1, ha.2]  · rw [dist_eq,zsmul_eq_mul, sub_sub_sub_cancel_right, ← dist_eq]    exact hxy.trans_le (min_le_left ..)  · constructor <;> linarith [ha.1, ha.2]