have : (p.sign * q).natAbs = q.natAbs := by
  rw [Int.natAbs_mul, Int.natAbs_sign_of_nonzero pprime.ne_zero, one_mul]
case neg.intro.intro.intro.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
⊢ ∃ p, |f| = p.norm
case neg.intro.intro.intro.intro.intro.intro
f : ℤ
hodd : Odd f
a : ℤ√(-3)
H : ¬Even a.norm
p : ℤ
pprime : Prime p
this✝ : p ∣ a.norm
podd : Odd p
A : ℤ√(-3)
HA : |p| = A.norm
pprime' : Prime A.norm
pdvd' : A.norm ∣ a.norm
c : ℤ√(-3)
hcd : a.norm = A.norm * c.norm
q : ℤ
hgpos : p * q ≠ 0
hfactor : f * (p * q) = a.norm
hnotform : ∀ (f' : ℤ), f' ∣ p * q → Odd f' → ∃ p, |f'| = p.norm
IH :
  ∀ m < (p * q).natAbs,
    ∀ (a : ℤ√(-3)) (g : ℤ),
      ¬g = 0 → f * g = a.norm → (∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, |f'| = p.norm) → g.natAbs = m → ∃ p, |f| = p.norm
h : ¬(p * q).natAbs = 1
hqpos : q ≠ 0
this : (p.sign * q).natAbs = q.natAbs
⊢ ∃ p, |f| = p.norm