convert (derivWithin_of_mem_uIoo ht).symm using 3
case h.e'_2.h
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ (fun t => deriv f t) t = (fun t => derivWithin f (Icc a b) t) t
case h.e'_3.h.e.h.e'_7
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t✝ : ℝ
n : ℕ
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ℝ → E
g : ℝ → ℝ
h : ContDiffOn ℝ 1 f (Icc a b)
hab : a ≤ b
t : ℝ
ht : t ∈ uIoo a b
⊢ Icc a b = uIcc a b