no goals
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
f : ℝ → F
K : Set F
inst✝ : CompleteSpace F
⊢ MeasurableSet {x | DifferentiableWithinAt ℝ f (Ioi x) x}
simpa [differentiableWithinAt_Ioi_iff_Ici] using measurableSet_of_differentiableWithinAt_Ici f