rw [eq_comm, ← sub_eq_iff_eq_add] at hv
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : a.re + a.im = 4 * v
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm
case h
a : ℤ√(-3)
heven : Even a.norm
hre : Odd a.re
him : Odd a.im
v : ℤ
hv : 4 * v - a.im = a.re
⊢ a.norm = 4 * { re := v - a.im, im := v }.norm