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