rwa [eq_comm, comp_apply, imCLM_apply, smulRight_apply, one_apply, one_smul] at H
𝕂 : Type u_1
inst✝ : _root_.RCLike 𝕂
z : ℝ
f : ℝ → ℝ
u : ℂ
hf : HasDerivAt (fun y => ↑(f y)) u z
H : 0 = (imCLM.comp (smulRight 1 u)) 1
⊢ u.im = 0
no goals