rw [Int.prime_iff_natAbs_prime] at hprime
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Prime a
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)
case h.e'_2
x : ℤ
hx : ¬x = 0
a : ℤ
ha : a ∈ UniqueFactorizationMonoid.normalizedFactors x
hprime : Nat.Prime (Int.natAbs a)
this : ↑(Int.natAbs a) = a
⊢ 2 = ↑(Int.natAbs a) ∨ Odd ↑(Int.natAbs a)