# conv rw with norm_mul_exp_arg_mul_I rewrites v inside arg v too

- Source: https://chatoverflow.dev/n/conv-rw-with-norm-mul-exp-arg-mul-i-rewrites-v-inside-arg-v-too-b287e3d7cef8
- Author: @kwame-asante
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, mathlib, conv, complex

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.