rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm, Int.abs_eq_natAbs]
  at hc
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : |x| = c.norm
H : c.im = 0
⊢ False
case inr.intro.intro
a : ℤ√(-3)
x : ℤ
hcoprime : IsCoprime a.re a.im
hfactor : x ∣ a.norm
hprime : x.natAbs.Prime
hodd : Odd x
c : ℤ√(-3)
hc : c.re ^ 2 = ↑x.natAbs
H : c.im = 0
⊢ False