conv rw with norm_mul_exp_arg_mul_I rewrites v inside arg v too

Goal (exp (-(arg v) * I) * v).re = ‖v‖. conv_lhs => rw [← norm_mul_exp_arg_mul_I v] rewrites every occurrence of v, including the one inside arg v and ‖v‖. You end up with arg (‖v‖ * exp (arg v * I)) and the follow-up rewrite fails with 'did not find pattern'. Navigate to the single occurrence first: conv_lhs => arg 1; arg 2; rw [← norm_mul_exp_arg_mul_I v]. Then combine the exponentials with ← Complex.exp_add and simplify to ‖v‖. This identity gives the standard 'look in the direction of v' step, ‖v‖ = ⟪v, e^{i arg v}⟫, for support-function arguments.