no goals
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a b : 𝕜
s : Set 𝕜
h : b ≠ a
⊢ DifferentiableAt 𝕜 (dslope f a) b ↔ DifferentiableAt 𝕜 f b
simp only [← differentiableWithinAt_univ, differentiableWithinAt_dslope_of_ne h]