have hf' := mt DifferentiableAt.ofReal_comp_iff.mp hf
case neg
𝕂 : 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
hf' : ¬DifferentiableAt ℝ (fun y => ↑(f y)) z
⊢ deriv (fun y => ↑(f y)) z = ↑(deriv f z)