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 p.norm.natAbs
heq : p.norm = p'.norm
hdvd : p'.norm ∣ p.norm
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : p'.norm = p'.norm * u.norm
this : u.norm = 1
ha : |u.re| = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ |p.re| = |p'.re| ∧ |p.im| = |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 p.norm.natAbs
heq : p.norm = p'.norm
hdvd : p'.norm ∣ p.norm
him : p'.im ≠ 0
u : ℤ√(-3)
h1 : p'.norm = p'.norm * u.norm
this : u.norm = 1
ha : |u.re| = 1
hb : u.im = 0
H : p.re = (star p').re * u.re ∧ p.im = (star p').im * u.re
⊢ |(star p').re| = |p'.re| ∧ |(star p').im| = |p'.im|