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