simp only [huv, Multiset.prod_cons, ← mul_neg]
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ a = Multiset.prod (q ::ₘ g) ∨ a = -Multiset.prod (q ::ₘ g)
case h.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.refine'_1
a✝ : ℤ√(-3)
hcoprime✝ : IsCoprime a✝.re a✝.im
n✝ : ℕ
hn✝ : Int.natAbs (Zsqrtd.norm a✝) = n✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {a : ℤ√(-3)},
        IsCoprime a.re a.im →
          Int.natAbs (Zsqrtd.norm a) = m →
            ∃ f,
              (a = Multiset.prod f ∨ a = -Multiset.prod f) ∧
                ∀ (pq : ℤ√(-3)), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : Int.natAbs (Zsqrtd.norm a) = n
h : Zsqrtd.norm a ≠ 1
U q : ℤ√(-3)
hc : 0 ≤ q.re
hd : q.im ≠ 0
hp : OddPrimeOrFour (Zsqrtd.norm q)
huv : a = q * U
huvcoprime : IsCoprime U.re U.im
descent : Int.natAbs (Zsqrtd.norm U) < n
g : Multiset (ℤ√(-3))
hgprod : U = Multiset.prod g ∨ U = -Multiset.prod g
hgfactors : ∀ (pq : ℤ√(-3)), pq ∈ g → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
⊢ q * U = q * Multiset.prod g ∨ q * U = q * -Multiset.prod g