rwa [← Int.coe_natAbs x, Int.natAbs_pow_two x, ← Int.coe_natAbs,
  Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) c)]
case intro.intro.intro.refine'_2.intro
x : ℤ
hodd : Odd x
h : 1 < abs x
c m : ℤ√(-3)
h2 : Zsqrtd.norm c < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ Zsqrtd.norm (c + m * ↑x)
y : ℤ
hy : Zsqrtd.norm c = x * y
h0'' : 0 < Int.natAbs x
⊢ abs (Zsqrtd.norm c) < abs x ^ 2
no goals