have HAsq : (A : ℤ) ^ 2 = 1 := by
  calc
    (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm
    _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A))
    _ = 1 := Units.val_one
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
case intro.intro
a p : ℤ√(-3)
hpprime : Prime (Zsqrtd.norm p)
f : ℤ
hf : Zsqrtd.norm a = Zsqrtd.norm p * f
h0 : Zsqrtd.norm p ∣ p.re * a.im - a.re * p.im ∨ Zsqrtd.norm p ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : Zsqrtd.norm p ∣ p.re * a.im + ↑A * a.re * p.im
HAsq : ↑A ^ 2 = 1
⊢ ∃ u, a = p * u ∨ a = star p * u