have : Even (evenFactorExp r) :=
  by
  suffices Even (3 * evenFactorExp r)
    by
    rw [Nat.even_mul] at this
    apply this.resolve_left
    norm_num; decide
  rw [← evenFactorExp.pow r 3, hcube]
  exact factors_2_even' hcoprime
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)
case h.e'_4
a : ℤ√(-3)
r : ℕ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = a.norm.natAbs
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = f.prod ∨ a = -f.prod
h2 : ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.count x f = 3 * Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)