cases' h1 with h1 h1 <;> rw [h1] at hcoprime
case h.e'_4.calc_1.hcoprime
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
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im
case h.e'_4.calc_1.hcoprime.inl
a : ℤ√(-3)
r : ℤ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (Multiset.prod f).re (Multiset.prod f).im
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
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im

case h.e'_4.calc_1.hcoprime.inr
a : ℤ√(-3)
r : ℤ
hcoprime✝ : IsCoprime a.re a.im
hcube : r ^ 3 = Zsqrtd.norm a
f : Multiset (ℤ√(-3)) := factorization' hcoprime✝
hcoprime : IsCoprime (-Multiset.prod f).re (-Multiset.prod f).im
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
h2x : 0 ≤ x.re ∧ x.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm x)
h : Zsqrtd.norm x = Zsqrtd.norm A
hassoc : Associated' x A
eq_or_eq_conj : x = A ∨ x = star A
H : x = star A
h1 : a = -Multiset.prod f
⊢ IsCoprime (Multiset.prod f).re (Multiset.prod f).im