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