case mpr =>
  intro (_ : Positive (-a))
  show Negative a
  have : NonzeroWithSign (-a) 1 := positive_iff_sign_pos1.mp ‹Positive (-a)›
  have : NonzeroWithSign a (-1) :=
    nonzeroWithSign_swap_neg.mp ‹NonzeroWithSign (-a) 1›
  have : Negative a := negative_iff_sign_neg1.mpr ‹NonzeroWithSign a (-1)›
  exact this
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a : ℤ
⊢ Positive (-a) → Negative a
no goals