rw [Zsqrtd.norm_mul]
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f * ↑u).norm
case intro
d : ℤ
f : ℤ√d
u : (ℤ√d)ˣ
this : IsUnit (↑u).norm
⊢ Associated f.norm (f.norm * (↑u).norm)