rw [derivWithin, deriv, fderivWithin_of_mem_nhds (uIcc_mem_nhds ht)]
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n : ℕ
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f✝ g f : ℝ → E
ht : t ∈ uIoo a b
⊢ derivWithin f (uIcc a b) t = deriv f t
no goals