rw [comp_apply, smulRight_apply, one_apply, one_smul, reCLM_apply, ofReal_re]
case h.e'_7
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt (fun y => ↑(f y)) (↑u) z
⊢ u = (reCLM.comp (smulRight 1 ↑u)) 1
no goals