exact absurd hpq (Multiset.not_mem_zero _)
case h.inl.right
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
pq : ℤ√(-3)
hpq : pq ∈ 0
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour (Zsqrtd.norm pq)
no goals