obtain ⟨y, hy, rfl⟩ := Multiset.mem_map.mp hx
case h.e'_4.calc_2.e_s.hf
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)
x : ℕ
hx : x ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour x
case h.e'_4.calc_2.e_s.hf.intro.intro
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)
y : ℤ√(-3)
hy : y ∈ f
hx : (Int.natAbs ∘ Zsqrtd.norm) y ∈ Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f
⊢ OddPrimeOrFour ((Int.natAbs ∘ Zsqrtd.norm) y)