apply (hg.differentiableOn le_rfl t (uIoo_subset_uIcc ht)).hasDerivWithinAt.mono_of_mem
𝕜 : 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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ HasDerivWithinAt g (derivWithin g (uIcc a b) t) (Ioi t) t
𝕜 : 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 : ℝ → ℝ
hg : ContDiffOn ℝ 1 g (uIcc a b)
hf : ContinuousOn f (g '' uIcc a b)
t : ℝ
ht : t ∈ Ioo (min a b) (max a b)
⊢ uIcc a b ∈ 𝓝[>] t