convert hp using 2 <;> simp <;> ring
case intro
a b r : ℤ
hcoprime : IsCoprime a b
hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2
A : ℤ√(-3) := { re := a, im := b }
hA : A = { re := a, im := b }
hcube' : r ^ 3 = Zsqrtd.norm A
p : ℤ√(-3)
hp :
  a =
      (((p ^ 0).re * p.re + -3 * (p ^ 0).im * p.im) * p.re + -3 * ((p ^ 0).re * p.im + (p ^ 0).im * p.re) * p.im) *
          p.re +
        -3 * (((p ^ 0).re * p.re + -3 * (p ^ 0).im * p.im) * p.im + ((p ^ 0).re * p.im + (p ^ 0).im * p.re) * p.re) *
          p.im ∧
    b =
      (((p ^ 0).re * p.re + -3 * (p ^ 0).im * p.im) * p.re + -3 * ((p ^ 0).re * p.im + (p ^ 0).im * p.re) * p.im) *
          p.im +
        (((p ^ 0).re * p.re + -3 * (p ^ 0).im * p.im) * p.im + ((p ^ 0).re * p.im + (p ^ 0).im * p.re) * p.re) * p.re
⊢ a = p.re ^ 3 - 9 * p.re * p.im ^ 2 ∧ b = 3 * p.re ^ 2 * p.im - 3 * p.im ^ 3
no goals