have podd : Odd p :=
  Int.odd_iff_not_even.mpr
    (by
      intro X
      apply H
      apply even_iff_two_dvd.mpr
      apply dvd_trans _ this
      apply even_iff_two_dvd.mp X)
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
⊢ ∃ p, abs f = Zsqrtd.norm p
case neg.intro.intro
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)
g : ℤ
hgpos : g ≠ 0
hfactor : f * g = Zsqrtd.norm a
hnotform : ∀ (f' : ℤ), f' ∣ g → Odd f' → ∃ p, abs f' = Zsqrtd.norm p
IH :
  ∀ (m : ℕ),
    m < Int.natAbs g →
      ∀ (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 : ¬Even (Zsqrtd.norm a)
h : ¬Int.natAbs g = 1
p : ℤ
pprime : Prime p
pdvd : p ∣ g
this : p ∣ Zsqrtd.norm a
podd : Odd p
⊢ ∃ p, abs f = Zsqrtd.norm p