obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im :=
  by
  cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;>
    simp only [Units.val_neg, Units.val_one, neg_mul, one_mul]
  ring
case intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u
case intro.intro
a p : ℤ√(-3)
hpprime : Prime p.norm
f : ℤ
hf : a.norm = p.norm * f
h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im
A : ℤˣ
HA : p.norm ∣ p.re * a.im + ↑A * a.re * p.im
⊢ ∃ u, a = p * u ∨ a = star p * u