by_cases hf : DifferentiableAt ℝ f z
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)
case pos
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)

case neg
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
hf : ¬DifferentiableAt ℝ f z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)