case mp =>
  intro (_ : Nonzero a)
  show Positive a ∨ Negative a
  have (Nonzero.intro (s : ℤ) (_ : Sqrt1 s) nwsa) := ‹Nonzero a›
  have : NonzeroWithSign a s := nwsa
  have : NonzeroWithSign a 1 ∨ NonzeroWithSign a (-1) :=
    nonzeroWithSign_cases ‹NonzeroWithSign a s›
  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 : ℤ
⊢ Nonzero a → Positive a ∨ Negative a
no goals