rwa [← Int.natCast_natAbs x, Int.natAbs_pow_two x, ← Int.natCast_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 < |x|
c m : ℤ√(-3)
h2 : c.norm < x ^ 2
hcoprime : IsCoprime (c + m * ↑x).re (c + m * ↑x).im
hfactor : x ∣ (c + m * ↑x).norm
y : ℤ
hy : c.norm = x * y
h0'' : 0 < x.natAbs
⊢ |c.norm| < |x| ^ 2
no goals