rw [hu', Zsqrtd.norm_mul]
case intro.refine'_2.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm a = 4 * Zsqrtd.norm u'
case intro.refine'_2.inr
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
heven : Even (Zsqrtd.norm a)
u' : ℤ√(-3)
hu' : a = { re := 1, im := -1 } * u'
⊢ Zsqrtd.norm { re := 1, im := -1 } * Zsqrtd.norm u' = 4 * Zsqrtd.norm u'