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