rw [hn, even_iff_two_dvd]
case h.e'_3
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
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ Even a.norm.natAbs
case h.e'_3
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
hfactor : 2 ∈ UniqueFactorizationMonoid.normalizedFactors n
⊢ 2 ∣ n