Theorem: derivWithin_of_mem_uIoo (RMT4/to_mathlib.lean)

State before:
𝕜 : 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
Tactic:
rw [derivWithin, deriv, fderivWithin_of_mem_nhds (uIcc_mem_nhds ht)]
State after:
no goals