case mpr =>
  intro (Exists.intro (y : ℚ) (And.intro (_ : Positive y) (_ : x ≃ -y)))
  show Negative x
  have : sgn y ≃ 1 := Rational.sgn_positive.mp ‹Positive y›
  have : sgn x ≃ -1 := calc
    sgn x      ≃ _ := Rational.sgn_subst ‹x ≃ -y›
    sgn (-y)   ≃ _ := Rational.sgn_compat_neg
    (-(sgn y)) ≃ _ := AA.subst₁ ‹sgn y ≃ 1›
    (-1)       ≃ _ := Rel.refl
  have : Negative x := Rational.sgn_negative.mpr this
  exact this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ (∃ y, Positive y ∧ x ≃ -y) → Negative x
no goals