case mpr =>
  intro (_ : AltNegative x)
  show Negative x
  have
    (AltNegative.intro
      (a : ℤ) (b : ℤ)
      (_ : AP (Positive a)) (_ : AP (Positive b)) x_eqv_neg_a_over_b)
    := ‹AltNegative x›
  have : x ≃ (-a) / b := x_eqv_neg_a_over_b
  have : AltPositive ((a : ℚ) / b) := AltPositive.mk Rational.eqv_refl
  have : Positive ((a : ℚ) / b) := alt_positive.mpr this
  have : x ≃ -((a : ℚ) / b) := calc
    x                ≃ _ := ‹x ≃ (-a) / b›
    (-a : ℚ) / b     ≃ _ := Rational.eqv_symm Rational.neg_scompatL_div
    (-((a : ℚ) / b)) ≃ _ := Rational.eqv_refl
  have : ∃ (y : ℚ), Positive y ∧ x ≃ -y :=
    Exists.intro ((a : ℚ) / b) (And.intro ‹Positive ((a : ℚ) / b)› this)
  have : Negative x := negative_iff_neg_positive.mpr this
  exact this
ℚ : Type
inst✝ : Rational ℚ
x : ℚ
⊢ AltNegative x → Negative x
no goals