Measurability of arctan

theorem Real.measurable_arctan : Measurable Real.arctan

theorem Measurable.arctan {α : Type u_1} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable f) : Measurable fun (x : α) => Real.arctan (f x)