case mpr =>
  intro (_ : Positive a ∨ Negative a)
  show Nonzero a
  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 : ℤ
⊢ Positive a ∨ Negative a → Nonzero a
no goals