rwa [← Int.natAbs_eq_zero, this, Int.natAbs_eq_zero]
case neg.intro.intro.intro.intro.intro.intro.refine'_2
a✝ : ℤ√(-3)
f g : ℤ
hodd : Odd f
hgpos✝ : g ≠ 0
hfactor✝ : f * g = Zsqrtd.norm a✝
hnotform✝ : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
x✝ : ℕ
hg : Int.natAbs g = x✝
a : ℤ√(-3)
H : ¬Even (Zsqrtd.norm a)
p : ℤ
pprime : Prime p
this✝ : p ∣ Zsqrtd.norm a
podd : Odd p
A : ℤ√(-3)
HA : abs p = Zsqrtd.norm A
pprime' : Prime (Zsqrtd.norm A)
pdvd' : Zsqrtd.norm A ∣ Zsqrtd.norm a
c : ℤ√(-3)
hcd : Zsqrtd.norm a = Zsqrtd.norm A * Zsqrtd.norm c
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs (p * q) →
      ∀ (a : ℤ√(-3)) (g : ℤ),
        ¬g = 0 →
          f * g = Zsqrtd.norm a →
            (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p) → Int.natAbs g = m → ∃ p, abs f = Zsqrtd.norm p
h : ¬Int.natAbs (p * q) = 1
hqpos : q ≠ 0
this : Int.natAbs (Int.sign p * q) = Int.natAbs q
⊢ ¬Int.sign p * q = 0
no goals