exact absurd hpq (Multiset.not_mem_zero _)
case h.right
n : ℕ
ih :
  ∀ m < n,
    ∀ {a : ℤ√(-3)},
      IsCoprime a.re a.im →
        a.norm.natAbs = m →
          ∃ f, (a = f.prod ∨ a = -f.prod) ∧ ∀ pq ∈ f, 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
a : ℤ√(-3)
hcoprime : IsCoprime a.re a.im
hn : a.norm.natAbs = n
h : a.norm = 1
pq : ℤ√(-3)
hpq : pq ∈ 0
⊢ 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs
no goals