show
  Multiset.countp (Eq x.norm) (Multiset.map Zsqrtd.norm f) =
    Multiset.countp (Eq x.norm) (factorsOddPrimeOrFour a.norm)
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countp (fun x_1 => Zsqrtd.norm x = x_1) (Multiset.map Zsqrtd.norm f) =
    Multiset.countp (fun x_1 => Zsqrtd.norm x = x_1) (factorsOddPrimeOrFour (Zsqrtd.norm a))

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ Zsqrtd.norm x = Zsqrtd.norm A
case h.e'_4.calc_2
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
⊢ Multiset.countp (Eq (Zsqrtd.norm x)) (Multiset.map Zsqrtd.norm f) =
    Multiset.countp (Eq (Zsqrtd.norm x)) (factorsOddPrimeOrFour (Zsqrtd.norm a))

case h.e'_4.calc_1
a : ℤ√(-3)
r : ℤ
hcoprime : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime
h1 : a = Multiset.prod f ∨ a = -Multiset.prod f
h2 : ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
hf : f = factorization' hcoprime
x : ℤ√(-3)
hx : x ∈ f
this : Even (evenFactorExp r)
A : ℤ√(-3)
HA : A ∈ f
⊢ x = A ↔ Zsqrtd.norm x = Zsqrtd.norm A