rw [H.1, H.2, abs_mul, abs_mul, ha, mul_one, mul_one]
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs p.re = abs p'.re ∧ abs p.im = abs p'.im
case intro.intro.intro.inr.intro
p p' : ℤ√(-3)
hcoprime : IsCoprime p.re p.im
hcoprime' : IsCoprime p'.re p'.im
h : OddPrimeOrFour (Zsqrtd.norm p)
heq : Zsqrtd.norm p = Zsqrtd.norm p'
hdvd : Zsqrtd.norm p' ∣ Zsqrtd.norm p
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : Zsqrtd.norm p' = Zsqrtd.norm p' * Zsqrtd.norm u
this : Zsqrtd.norm u = 1
ha : abs u.re = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ abs (star p').re = abs p'.re ∧ abs (star p').im = abs p'.im