match ‹Positive a ∨ Negative a› with
| Or.inl (_ : Positive a) =>
  have : NonzeroWithSign a 1 := positive_iff_sign_pos1.mp ‹Positive a›
  exact Nonzero.mk ‹NonzeroWithSign a 1›
| Or.inr (_ : Negative a) =>
  have : NonzeroWithSign a (-1) := negative_iff_sign_neg1.mp ‹Negative a›
  exact Nonzero.mk ‹NonzeroWithSign a (-1)›
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
x✝ : Positive a ∨ Negative a
⊢ Nonzero a
no goals