rw [huvprod, factors_2_even huv, Nat.even_add]
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even (evenFactorExp (Zsqrtd.norm a))
case pos.intro.intro
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
x✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n → ∀ {a : ℤ√(-3)}, IsCoprime a.re a.im → Int.natAbs (Zsqrtd.norm a) = m → Even (evenFactorExp (Zsqrtd.norm a))
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
hparity : Even (Zsqrtd.norm a)
u : ℤ√(-3)
huvcoprime : IsCoprime u.re u.im
huvprod : Zsqrtd.norm a = 4 * Zsqrtd.norm u
huv : Zsqrtd.norm u ≠ 0
⊢ Even 2 ↔ Even (evenFactorExp (Zsqrtd.norm u))